Commit 2025-12-16 07:57 8e30505e

View on Github →

feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group (#26831) This proves the first case (intransitive) of the O'Nan-Scott classification of maximal subgroups of the alternating group.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Set.one_lt_ncard_iff_nontrivial

added theorem Set.one_lt_ncard_iff_nontrivial_and_finite

Modified Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

deleted theorem SubMulAction.ofStabilizer.AlternatingGroup.isMultiplyPretransitive

deleted theorem SubMulAction.ofStabilizer.AlternatingGroup.isPreprimitive_of_three_le_card

deleted theorem SubMulAction.ofStabilizer.AlternatingGroup.isPretransitive_of_three_le_card

deleted theorem SubMulAction.ofStabilizer.AlternatingGroup.isTrivialBlock_of_isBlock

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

Modified Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

deleted theorem Equiv.Perm.IsPretransitive.of_partition

added theorem Equiv.Perm.exists_mem_stabilizer_smul_eq

deleted theorem Equiv.Perm.moves_in

modified theorem Equiv.Perm.ofSubtype_mem_stabilizer

added theorem Equiv.Perm.stabilizer.surjective_toPerm

deleted theorem IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl

deleted theorem IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_le

deleted theorem IsBlock.subsingleton_of_stabilizer_lt_of_subset

added theorem MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl

added theorem MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_Perm_le

added theorem MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le

added theorem MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset

added theorem MulAction.IsPretransitive.of_partition

added theorem MulAction.isPreprimitive_stabilizer_of_surjective

added theorem MulAction.isPreprimitive_stabilizer_subgroup

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

added theorem Equiv.Perm.mul_mem_alternatingGroup_of_isSwap

Created Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean

added theorem Equiv.Perm.alternatingGroup_le_of_isPreprimitive

added theorem Equiv.Perm.exists_mem_stabilizer_isThreeCycle

added theorem Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard

added theorem MulAction.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le

added theorem alternatingGroup.exists_mem_stabilizer_smul_eq

added theorem alternatingGroup.isCoatom_stabilizer

added theorem alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl

added theorem alternatingGroup.isCoatom_stabilizer_singleton

added theorem alternatingGroup.stabilizer.surjective_toPerm

added theorem alternatingGroup.stabilizer_isPreprimitive

added theorem alternatingGroup.stabilizer_ne_top

added theorem alternatingGroup.stabilizer_subgroup_isPreprimitive

added theorem alternatingGroup.subgroup_eq_top_of_isPreprimitive