Commit 2024-02-12 10:30 8a5da17d

View on Github →

feat(GroupTheory/GroupAction): new FixedPoints module with a few basic properties of fixedBy (#9477) Introduces a new module, Mathlib.GroupTheory.GroupAction.FixedPoints, which contains some properties of MulAction.fixedBy that wouldn't quite belong to Mathlib.GroupTheory.GroupAction.Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.smul_set_compl

Created Mathlib/GroupTheory/GroupAction/FixedPoints.lean

added theorem MulAction.fixedBy_eq_univ_iff_eq_one

added theorem MulAction.fixedBy_inv

added theorem MulAction.fixedBy_mem_fixedBy_of_commute

added theorem MulAction.fixedBy_mul

added theorem MulAction.fixedBy_one_eq_univ

added theorem MulAction.fixedBy_subset_fixedBy_zpow

added theorem MulAction.minimalPeriod_eq_one_iff_fixedBy

added theorem MulAction.movedBy_mem_fixedBy_of_commute

added theorem MulAction.not_commute_of_disjoint_movedBy_preimage

added theorem MulAction.set_mem_fixedBy_iff

added theorem MulAction.set_mem_fixedBy_of_movedBy_subset

added theorem MulAction.set_mem_fixedBy_of_subset_fixedBy

added theorem MulAction.smul_fixedBy

added theorem MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy

added theorem MulAction.smul_mem_fixedBy_iff_mem_fixedBy

added theorem MulAction.smul_mem_of_set_mem_fixedBy

added theorem MulAction.smul_subset_of_set_mem_fixedBy

added theorem MulAction.smul_zpow_fixedBy_eq_of_commute

added theorem MulAction.smul_zpow_movedBy_eq_of_commute

Modified Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

added theorem mem_fixingSubgroup_compl_iff_movedBy_subset

added theorem mem_fixingSubgroup_iff_subset_fixedBy

added theorem orbit_fixingSubgroup_compl_subset