mathlib3

54eccb0e - feat(measure_theory/lp_space): add snorm_eq_lintegral_rpow_nnnorm (#8115)

feat(measure_theory/lp_space): add snorm_eq_lintegral_rpow_nnnorm (#8115) Add two lemmas to go from `snorm` to integrals (through `snorm'`). The idea is that `snorm'` should then generally not be used, except in the construction of `snorm`.