Commit 2026-04-28 15:42 d6bd04b5

feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) This is the conclusion of the story of the proof of simplicity of the alternating group using the Iwasawa criterion.

• Equiv.Perm.iwasawaStructure_two: the natural IwasawaStructure of Equiv.Perm α acting on Nat.Combination α 2 Its commutative subgroups consist of the permutations with support in a given element of Nat.Combination α 2. They are cyclic of order 2.
• alternatingGroup_of_le_of_normal: If α has at least 5 elements, then a nontrivial normal subgroup of Equiv.Perm α contains the alternating group.
• alternatingGroup.iwasawaStructure_three: the natural IwasawaStructure of alternatingGroup α acting on Nat.Combination α 3 Its commutative subgroups consist of the permutations with support in a given element of Nat.Combination α 2. They are cyclic of order 3.
• alternatingGroup.iwasawaStructure_three: the natural IwasawaStructure of alternatingGroup α acting on Nat.Combination α 4 Its commutative subgroups consist of the permutations of cycleType (2, 2) with support in a given element of Nat.Combination α 2. They have order 4 and exponent 2 (IsKleinFour).
• alternatingGroup.normal_subgroup_eq_bot_or_eq_top: If α has at least 5 elements, then a nontrivial normal subgroup of alternatingGroup is ⊤.
• alternatingGroup.isSimpleGroup: If α has at least 5 elements, then alternatingGroup α is a simple group.