English
In the setting of Equiv.Perm, the statement that toList f x forms the permutation equal to cycleOf f x.
Русский
В контексте Equiv.Perm, toList f x образует перестановку, равную cycleOf f x.
LaTeX
$$$$\mathrm{formPerm}(\mathrm{toList}\ f\ x) = f.cycleOf x.$$$$
Lean4
/-- Given a cyclic `f : Perm α`, generate the `Cycle α` in the order
of application of `f`. Implemented by finding an element `x : α`
in the support of `f` in `Finset.univ`, and iterating on using
`Equiv.Perm.toList f x`.
-/
def toCycle (f : Perm α) (hf : IsCycle f) : Cycle α :=
Multiset.recOn (Finset.univ : Finset α).val (Quot.mk _ []) (fun x _ l => if f x = x then l else toList f x)
(by
intro x y _ s
refine heq_of_eq ?_
split_ifs with hx hy hy <;> try rfl
have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
exact Quotient.sound' hc.toList_isRotated)
