mathlib3

8377a1fc - feat(measure_theory/lp_space): add snorm_le_snorm_mul_rpow_measure_univ (#7926)

feat(measure_theory/lp_space): add snorm_le_snorm_mul_rpow_measure_univ (#7926) There were already versions of this lemma for `snorm'` and `snorm_ess_sup`. The new lemma collates these into a statement about `snorm`.