Theorem alternatingGroup.isMulCommutative_iff_card_le_three

Modification history

2026-04-28 15:42
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) …
Added alternatingGroup.isMulCommutative_iff_card_le_threeView on Github →