Commit 2025-10-04 20:24 9bee9f3e

View on Github →

feat: a theorem of Jordan on primitive subgroups of the permutation group (#26282) A theorem of Jordan on the primitive subgroups of a permutation group:

if it contains a swap, it is equal to the permutation group,
if it contains a 3-cycle, it contains the alternating group. This PR continues the work from #24131.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Set.ncard_le_card

added theorem Set.ncard_lt_card

added theorem Set.ncard_range_of_injective

added theorem Set.ncard_union_eq_iff

added theorem Set.ncard_union_lt

added theorem Set.nonempty_inter_compl_of_ncard_add_ncard_lt

added theorem Set.nonempty_inter_of_le_ncard_add_ncard

added theorem Set.nonempty_inter_of_lt_ncard_add_ncard

added theorem Set.union_ne_univ_of_ncard_add_ncard_lt

Modified Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

added theorem fixingSubgroup_empty

Created Mathlib/GroupTheory/GroupAction/Jordan.lean

added theorem Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem

added theorem Equiv.Perm.eq_top_of_isPreprimitive_of_isSwap_mem

added theorem Equiv.Perm.isMultiplyPretransitive_of_nontrivial

added theorem Equiv.Perm.isPretransitive_of_isCycle_mem

added theorem Equiv.Perm.subgroup_eq_top_of_nontrivial

added theorem MulAction.IsPreprimitive.isMultiplyPreprimitive

added theorem MulAction.IsPreprimitive.is_two_motive_of_is_motive

added theorem MulAction.IsPreprimitive.is_two_preprimitive

added theorem MulAction.IsPreprimitive.is_two_pretransitive

added theorem normalClosure_of_stabilizer_eq_top

Modified Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

deleted theorem Equiv.Perm.eq_top_if_isMultiplyPretransitive

deleted theorem Equiv.Perm.isMultiplyPretransitive

added theorem IsMultiplyPretransitive.alternatingGroup_le

deleted theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive'

deleted theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive

added theorem SubMulAction.ofStabilizer.AlternatingGroup.isMultiplyPretransitive

added theorem SubMulAction.ofStabilizer.AlternatingGroup.isPreprimitive_of_three_le_card

added theorem SubMulAction.ofStabilizer.AlternatingGroup.isPretransitive_of_three_le_card

added theorem SubMulAction.ofStabilizer.AlternatingGroup.isTrivialBlock_of_isBlock

added theorem SubMulAction.ofStabilizer.Equiv.Perm.eq_top_of_isMultiplyPretransitive

added theorem SubMulAction.ofStabilizer.Equiv.Perm.isMultiplyPretransitive

added theorem SubMulAction.ofStabilizer.MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq

added theorem SubMulAction.ofStabilizer.MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul

added theorem SubMulAction.ofStabilizer.ofFixingSubgroup.isMultiplyPretransitive'

added theorem SubMulAction.ofStabilizer.ofFixingSubgroup.isMultiplyPretransitive

Modified Mathlib/GroupTheory/GroupAction/Primitive.lean

added theorem MulAction.isTrivialBlock_of_card_le_two

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

added theorem SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter

added theorem SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter

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

added theorem SubMulAction.ENat_card_ofStabilizer_add_one_eq

deleted theorem SubMulAction.Enat_card_ofStabilizer_eq_add_one

added theorem SubMulAction.nat_card_ofStabilizer_add_one_eq

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

added theorem Equiv.Perm.IsSwap.orderOf

added theorem Equiv.Perm.isSwap_iff_cycleType

Modified Mathlib/SetTheory/Cardinal/Embedding.lean

added theorem Fin.Embedding.restrictSurjective_of_le_ENatCard

added theorem Fin.Embedding.restrictSurjective_of_le_natCard