Mathlib Changelog
v4
Changelog
About
Github
Theorem
essSup_ennreal_smul_measure
Modification history
2026-01-20 08:34
Mathlib/MeasureTheory/Function/EssSup.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Added
essSup_ennreal_smul_measure
View on Github →