Commit 2025-07-07 17:19 f7deeff1

View on Github →

feat(GroupTheory/GroupAction/Jordan) : Primitivity lemmas (#26280) This is a primitivity lemma for actions, in preparation to the proof of of Jordan on primitive subgroups of the permutation group #26282 This PR continues the work from #24120. Original PR: https://github.com/leanprover-community/mathlib4/pull/24120

depends on: #26279

Estimated changes

Modified Mathlib/Algebra/Group/Action/End.lean

Modified Mathlib/Algebra/Group/Action/Pretransitive.lean

Modified Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

added theorem Equiv.Perm.eq_top_if_isMultiplyPretransitive

added theorem Equiv.Perm.isMultiplyPretransitive

added theorem MulAction.isMultiplyPretransitive_iff

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean

modified theorem SubMulAction.ofFixingSubgroup_of_eq_apply

modified theorem SubMulAction.ofFixingSubgroup_of_eq_bijective

modified theorem SubMulAction.ofFixingSubgroup_of_inclusion_injective

modified theorem SubMulAction.ofFixingSubgroup_of_singleton_bijective