Commit 2024-07-18 01:57 2153e5ed

View on Github →

feat(AEStabilizer): new file (#14822)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Group/AEStabilizer.lean

added theorem MeasureTheory.inv_smul_ae_eq_self

added theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers

added def MulAction.aestabilizer

added theorem MulAction.aestabilizer_congr

added theorem MulAction.aestabilizer_empty

added theorem MulAction.aestabilizer_of_aeconst

added theorem MulAction.aestabilizer_univ

added theorem MulAction.mem_aestabilizer

added theorem MulAction.stabilizer_le_aestabilizer

Modified Mathlib/MeasureTheory/Group/Action.lean

deleted theorem MeasureTheory.inv_smul_ae_eq_self

deleted theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers

added theorem MeasureTheory.smul_set_ae_eq

added theorem MeasureTheory.smul_set_ae_le

deleted theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples

Modified Mathlib/MeasureTheory/Group/AddCircle.lean