Theorem MeasureTheory.eLpNormEssSup_ennreal_smul_measure

Modification history

2026-01-20 08:34
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Added MeasureTheory.eLpNormEssSup_ennreal_smul_measureView on Github →