English
There is a quotient-independent way to factor a permutation into a truncated list of disjoint cycles.
Русский
Существуют устойчивые разложения перестановки на усечённый список непересекающихся циклов.
LaTeX
$$$\\\\text{truncCycleFactors} : \\\\text{Trunc}{\\{ l : List (Perm α) // l.prod = f \\\\land ... \\}}$$$
Lean4
/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
without a linear order. -/
def truncCycleFactors [DecidableEq α] [Fintype α] (f : Perm α) :
Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
(show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
