Commit 2025-01-31 14:09 bd8a0b99

View on Github →

feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) A subgroup of index 2 of Equiv.Perm αis equal to alternatingGroup α, a subgroup of index at most 2 contains it.

Estimated changes

Modified Mathlib/GroupTheory/IndexNormal.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

added theorem Equiv.Perm.alternatingGroup_le_of_index_le_two

added theorem Equiv.Perm.eq_alternatingGroup_of_index_eq_two

added theorem alternatingGroup.eq_bot_of_card_le_two

added theorem alternatingGroup.index_eq_two

added theorem index_eq_one