Commit 2023-05-30 08:46 76b688b2

View on Github →

feat: port MeasureTheory.Group.Action (#4431)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/Action.lean

added theorem MeasureTheory.NullMeasurableSet.smul

added theorem MeasureTheory.locallyFiniteMeasure_of_smulInvariant

added theorem MeasureTheory.map_smul

added theorem MeasureTheory.measurePreserving_smul

added theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant

added theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero

added theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero

added theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant

added theorem MeasureTheory.measure_preimage_smul

added theorem MeasureTheory.measure_smul

added theorem MeasureTheory.measure_smul_null

added theorem MeasureTheory.smulInvariantMeasure_tfae

added theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers

added theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples