Theorem alternatingGroup.kleinFour_eq_commutator

Modification history

2025-07-23 08:49
Mathlib/GroupTheory/SpecificGroups/Alternating/KleinFour.lean
feat(GroupTheory/SpecificGroups/Alternating/KleinFour): the Klein Four subgroup of alternatingGroup on 4 letters (#27057) …
Added alternatingGroup.kleinFour_eq_commutatorView on Github →