English
For any permutation f, the formPerm of the toList f x equals the cycle Of f at x.
Русский
Для любой перестановки f: formPerm(toList f x) = cycleOf f x.
LaTeX
$$$$\mathrm{formPerm}(\mathrm{toList}\ f\ x) = f.cycleOf x.$$$$
Lean4
theorem formPerm_toList (f : Perm α) (x : α) : formPerm (toList f x) = f.cycleOf x :=
by
by_cases hx : f x = x
· rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx), formPerm_nil]
ext y
by_cases hy : SameCycle f x y
· obtain ⟨k, _, rfl⟩ := hy.exists_pow_eq_of_mem_support (mem_support.mpr hx)
rw [cycleOf_apply_apply_pow_self, List.formPerm_apply_mem_eq_next (nodup_toList f x), next_toList_eq_apply,
pow_succ', mul_apply]
rw [mem_toList_iff]
exact ⟨⟨k, rfl⟩, mem_support.mpr hx⟩
· rw [cycleOf_apply_of_not_sameCycle hy, formPerm_apply_of_notMem]
simp [mem_toList_iff, hy]
