mathlib3

0c8b8084 - fix(measure_theory/function/lp_space): fix an instance diamond in `measure_theory.Lp.has_edist` (#13388)

fix(measure_theory/function/lp_space): fix an instance diamond in `measure_theory.Lp.has_edist` (#13388) This also changes the definition of `edist` to something definitionally nicer Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>