Theorem Equiv.Perm.eq_alternatingGroup_of_index_eq_two

Modification history

2025-01-31 14:09
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) …
Added Equiv.Perm.eq_alternatingGroup_of_index_eq_twoView on Github →