Theorem MeasureTheory.Measure.ennreal_smul_eq_zero

Modification history

2026-08-20 12:42

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

chore: split too long file Measure.MeasureSpace (#42949) …

Modified MeasureTheory.Measure.ennreal_smul_eq_zero View on Github →

2026-01-20 08:34

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …

Added MeasureTheory.Measure.ennreal_smul_eq_zero View on Github →