Theorem commutator_alternatingGroup_eq_self

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 commutator_alternatingGroup_eq_selfView on Github →
2025-05-08 22:10
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
feat: more lemmas about alternatingGroup (#22576)
Added commutator_alternatingGroup_eq_selfView on Github →