cycleFactors — Mathlib

English

A permutation f is represented as a finite list of disjoint cycles whose product equals f.

Русский

Перестановка f представляется в виде конечного списка непересекающихся циклов, произведение которых равно f.

LaTeX

$$$f \\text{ cycle factors } = l \\text{ with } l.prod = f$$$

Lean4

/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  cycleFactorsAux (sort (α := α) (· ≤ ·) univ) f (fun {_ _} ↦ (mem_sort _).2 (mem_univ _))

Похожие утверждения