Theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure

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 Equiv.Perm.IsThreeCycle.alternating_normalClosureView on Github →
2026-04-28 15:42
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups (#36524) …
Modified Equiv.Perm.IsThreeCycle.alternating_normalClosureView on Github →
2023-04-12 21:22
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
feat: port GroupTheory.SpecificGroups.Alternating (#3371)
Added Equiv.Perm.IsThreeCycle.alternating_normalClosureView on Github →