mathlib3

acbb2a53 - feat(analysis/normed_space/pi_Lp): use typeclass inference for `1 ≤ p` (#9922)

feat(analysis/normed_space/pi_Lp): use typeclass inference for `1 ≤ p` (#9922) In `measure_theory.Lp`, the exponent `(p : ℝ≥0∞)` is an explicit hypothesis, and typeclass inference finds `[fact (1 ≤ p)]` silently (with the help of some pre-built `fact_one_le_two_ennreal` etc for specific use cases). Currently, in `pi_Lp`, the fact that `(hp : 1 ≤ p)` must be provided explicitly. I propose changing over to the `fact` system as used `measure_theory.Lp` -- I think it looks a bit prettier in typical use cases.