Theorem Equiv.Perm.IsThreeCycle.ne_one

Modification history

2026-05-10 10:59
Mathlib/GroupTheory/Perm/Cycle/Type.lean
chore(GroupTheory/SpecificGroups/Alternating): deprecate old proof of simplicity of A_5 (#38670) …
Added Equiv.Perm.IsThreeCycle.ne_oneView on Github →