Commit 2023-05-22 11:18 c59c263c

View on Github →

chore: forward-port leanprover-community/mathlib#18980 (#3956)

Estimated changes

Modified Mathlib/Data/Real/ENNReal.lean

added theorem ENNReal.smul_top

Modified Mathlib/MeasureTheory/Measure/OuterMeasure.lean

added theorem MeasureTheory.smul_extend

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.smul_iSup

added theorem ENNReal.smul_sSup