Theorem Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup

Modification history

2025-05-08 22:10
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
feat: more lemmas about alternatingGroup (#22576)
Added Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroupView on Github →