Theorem alternatingGroup.nontrivial_of_three_le_card

Modification history

2026-04-28 15:42
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) …
Modified alternatingGroup.nontrivial_of_three_le_cardView on Github →
2023-04-12 21:22
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat: port GroupTheory.SpecificGroups.Alternating (#3371)
Added alternatingGroup.nontrivial_of_three_le_cardView on Github →