Theorem MeasureTheory.Measure.isLocallyFiniteMeasure_smul

Modification history

2026-09-24 11:48
Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
chore(MeasureTheory): using ENNReal instead of NNReal (#42261) …
Added MeasureTheory.Measure.isLocallyFiniteMeasure_smulView on Github →