Theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure
Modification history
2025-04-15 10:46
Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
chore: split `MeasureTheory.Integral.SetToL1` (#24075) …
Modified MeasureTheory.DominatedFinMeasAdditive.of_smul_measureView on Github →