Theorem alternatingGroup.normalClosure_finRotate_five

Modification history

2026-05-10 10:59
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
chore(GroupTheory/SpecificGroups/Alternating): deprecate old proof of simplicity of A_5 (#38670) …
Modified alternatingGroup.normalClosure_finRotate_fiveView on Github →
2023-04-12 21:22
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat: port GroupTheory.SpecificGroups.Alternating (#3371)
Added alternatingGroup.normalClosure_finRotate_fiveView on Github →