Theorem alternatingGroup.commutator_perm_le

Modification history

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