Commit 2021-01-03 18:36 e1138b00
View on Github →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.