mathlib

e1138b00 - feat(measure_theory/lp_space): snorm is zero iff the function is zero ae (#5595)

feat(measure_theory/lp_space): snorm is zero iff the function is zero ae (#5595) Adds three lemmas, one for both directions of the iff, `snorm_zero_ae` and `snorm_eq_zero`, and the iff lemma `snorm_eq_zero_iff`.