Theorem Equiv.Perm.sign_ofSubtype

Modification history

2026-03-12 12:09
Mathlib/GroupTheory/Perm/Sign.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. (#33082) …
Modified Equiv.Perm.sign_ofSubtypeView on Github →
2023-02-27 13:06
Mathlib/GroupTheory/Perm/Sign.lean
feat: port GroupTheory.Perm.Sign (#2458)
Added Equiv.Perm.sign_ofSubtypeView on Github →