Def Equiv.Perm.cycleFactorsAux
Modification history
2025-01-24 08:47
Mathlib/GroupTheory/Perm/Cycle/Factors.lean
perf: improves the performance of the `Repr (Equiv.Perm α)` instance (2/4) (#20538) …
Modified Equiv.Perm.cycleFactorsAuxView on Github →2024-09-04 08:40
Mathlib/GroupTheory/Perm/Cycle/Factors.lean
chore: remove a superfluous by in `GroupTheory.Perm.Cycle.Factors` (#16465)
Modified Equiv.Perm.cycleFactorsAuxView on Github →2024-03-04 10:56
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
chore(GroupTheory/Perm/Cycle/Basic): Split (#10907) …
Modified Equiv.Perm.cycleFactorsAuxView on Github →