Theorem alternatingGroup.commutator_perm_eq

Modification history

2026-04-28 15:42
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) …
Modified alternatingGroup.commutator_perm_eqView on Github →
2025-05-08 22:10
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
feat: more lemmas about alternatingGroup (#22576)
Added alternatingGroup.commutator_perm_eqView on Github →