Commit 2025-10-07 08:33 29c47b65

View on Github →

chore(GroupTheory/Perm/Cycle): deprecate Disjoint.cycleType (#28429)

Estimated changes

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

deleted theorem Equiv.Perm.Disjoint.cycleType

modified theorem Equiv.Perm.Disjoint.cycleType_mul

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean