Commit 2024-07-20 19:54 6fdf9931

View on Github →

feat(MeasureTheory/../Action): drop measurability assumptions (#14933) Also reorder arguments of measure_preimage_smul and measure_smul.

Estimated changes

Modified Mathlib/MeasureTheory/Group/Action.lean

modified theorem MeasureTheory.measure_preimage_smul

added theorem MeasureTheory.measure_preimage_smul_le

added theorem MeasureTheory.measure_preimage_smul_null

added theorem MeasureTheory.measure_preimage_smul_of_nullMeasurableSet

modified theorem MeasureTheory.measure_smul

modified theorem MeasureTheory.measure_smul_eq_zero_iff

modified theorem MeasureTheory.measure_smul_null

added theorem MeasureTheory.tendsto_smul_ae

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

modified theorem MeasureTheory.IsFundamentalDomain.measure_ne_zero

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean