English
A permutation can be represented as a product of transpositions in a way that depends on a chosen linear order; for finite α there is a canonical extraction of such a list.
Русский
Перестановку можно представить как произведение транспозиций, зависящее от выбранного линейного порядка; существует каноническое представление такого списка для конечного α.
LaTeX
$$$ [Fintype\\ α]\\ [LinearOrder\\ α] \\to (f : Perm\\ α) \\to \\{ l : List (Perm\\ α) // l.prod = f \\wedge \\forall g \\in l, g.isSwap \\}$$$
Lean4
/-- `swapFactors` represents a permutation as a product of a list of transpositions.
The representation is nonunique and depends on the linear order structure.
For types without linear order `truncSwapFactors` can be used. -/
def swapFactors [Fintype α] [LinearOrder α] (f : Perm α) : { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g } :=
swapFactorsAux ((@univ α _).sort (· ≤ ·)) f fun {_ _} => (mem_sort _).2 (mem_univ _)
