Commit 2025-05-08 22:10 c2eae280

View on Github →

feat: more lemmas about alternatingGroup (#22576)

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

added theorem Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup

added theorem Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup

added theorem alternatingGroup.commutator_perm_eq

added theorem alternatingGroup.commutator_perm_le

added theorem commutator_alternatingGroup_eq_self

added theorem commutator_alternatingGroup_eq_top