Commit 2021-10-28 12:41 acbb2a53

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.