English
From a cycle factorization, construct a finite set of disjoint cycles representing f.
Русский
Из разложения на циклы получить конечное множество непересекающихся циклов, представляющих f.
LaTeX
$$$cycleFactorsFinset : Equiv.Perm α \\to Finset (Equiv.Perm α)$$$
Lean4
/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
-/
def cycleFactorsFinset : Finset (Perm α) :=
(truncCycleFactors f).lift
(fun l : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } =>
⟨↑l.val, nodup_of_pairwise_disjoint (fun h1 => not_isCycle_one <| l.2.2.1 _ h1) l.2.2.2⟩)
fun ⟨_, hl⟩ ⟨_, hl'⟩ =>
Finset.eq_of_veq <|
Multiset.coe_eq_coe.mpr <|
list_cycles_perm_list_cycles (hl'.left.symm ▸ hl.left) hl.right.left hl'.right.left hl.right.right
hl'.right.right
