Theorem Equiv.Perm.IsCycle.cycleType

Modification history

2025-03-29 18:40
Mathlib/GroupTheory/Perm/Cycle/Type.lean
chore(*): use `#s` notation here and there (#23438)
Modified Equiv.Perm.IsCycle.cycleTypeView on Github →
2025-03-11 22:28
Mathlib/GroupTheory/Perm/Cycle/Type.lean
chore(Mathlib/Data/List/Cycle, Mathlib/GroupTheory/Perm/Cycle/Type): use multiset singleton instead of list singleton (#22598) …
Modified Equiv.Perm.IsCycle.cycleTypeView on Github →
2023-04-05 09:20
Mathlib/GroupTheory/Perm/Cycle/Type.lean
feat: port GroupTheory.Perm.Cycle.Type (#3027)
Added Equiv.Perm.IsCycle.cycleTypeView on Github →