lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)

Commit

3 years ago

feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

Author

kex-y

Parents

dcedc047

mathlib 728e074e - feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)

mathlib
728e074e - feat(measure_theory/function/lp_order): prove a `normed_lattice_add_comm_group` instance for Lp (#14999)