English
Every permutation on a finite set can be written as a product of disjoint cycles. The decomposition is unique up to the order of the factors.
Русский
Каждая перестановка на конечном множестве раскладывается в произведение непересекающихся циклов. Разложение уникально по отношению к упорядочению циклаов.
LaTeX
$$$\\\\exists C_1, \\\\\\dots, C_k \\\\text{ cycles on } \\alpha \\\\, \\text{ with pairwise disjoint supports such that } f = C_1 \\\\cdot \\\\dots \\\\cdot C_k$$$
Lean4
/-- Represents a permutation as product of disjoint cycles:
```
#eval (c[0, 1, 2, 3] : Perm (Fin 4))
-- c[0, 1, 2, 3]
#eval (c[3, 1] * c[0, 2] : Perm (Fin 4))
-- c[0, 2] * c[1, 3]
#eval (c[1, 2, 3] * c[0, 1, 2] : Perm (Fin 4))
-- c[0, 2] * c[1, 3]
#eval (c[1, 2, 3] * c[0, 1, 2] * c[3, 1] * c[0, 2] : Perm (Fin 4))
-- 1
```
-/
unsafe instance instRepr [Repr α] : Repr (Perm α) where
reprPrec f
prec :=
-- Obtain a list of formats which represents disjoint cycles.
letI l :=
Quot.unquot <|
Multiset.map repr <|
Multiset.pmap toCycle (Perm.cycleFactorsFinset f).val fun _ hg =>
(mem_cycleFactorsFinset_iff.mp (Finset.mem_def.mpr hg)).left
match l with
| [] => "1"
| [f] => f
| l =>
-- multiple terms, use `*` precedence
(if prec ≥ 70 then Lean.Format.paren else id)
(Lean.Format.fill (Lean.Format.joinSep l (" *" ++ Lean.Format.line)))
