Commit 2026-03-12 12:09 d87f4555

View on Github →

feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. (#33082) This is preparatory material for the conclusion of the story of the proof of simplicity of the alternating group using the Iwasawa criterion which is #36524.

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

added theorem ConjAct.coe_smul

added theorem ConjAct.toConjAct_inv_smul

added theorem ConjAct.toConjAct_smul_eq_mulAut_conj

Modified Mathlib/GroupTheory/Perm/ConjAct.lean

added theorem Equiv.Perm.conj_smul_range_ofSubtype

added theorem Equiv.Perm.support_conj_eq_smul_support

Modified Mathlib/GroupTheory/Perm/Finite.lean

added theorem Equiv.Perm.mem_range_ofSubtype_iff

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified theorem Equiv.Perm.sign_ofSubtype

Modified Mathlib/GroupTheory/Perm/Support.lean

added theorem Equiv.Perm.mem_support_ofSubtype

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

deleted theorem Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup

added theorem Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup

added theorem Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroup

added theorem Equiv.Perm.isThreeCycle_subset_alternatingGroup

added theorem alternatingGroup.closure_cycleType_eq_two_two_eq_top

added theorem alternatingGroup.closure_isThreeCycles_eq_top

added theorem alternatingGroup.conj_smul_range_ofSubtype

added theorem alternatingGroup.map_ofSubtype

added theorem alternatingGroup.mem_range_ofSubtype_iff

added def alternatingGroup.ofSubtype

added theorem alternatingGroup.ofSubtype_comp_subtype

added theorem alternatingGroup.range_ofSubtype

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

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

added theorem IsKleinFour.isMulCommutative