Commit 2023-05-11 08:19 739f7dd5

View on Github →

feat: port MeasureTheory.Group.Pointwise (#3914)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Pointwise.lean

added theorem MeasurableSet.const_smul

added theorem MeasurableSet.const_smul_of_ne_zero

added theorem MeasurableSet.const_smul₀