English
Same as above for Equiv.Perm, expressing the rotation relation between toList and powers.
Русский
То же самое для Equiv.Perm: отношение поворота между toList и степенями перестановки.
LaTeX
$$$$\forall {\alpha} [Fintype \alpha] [DecidableEq \alpha] {p : Equiv.Perm \alpha} {x : \alpha} {k : \mathbb{N}},\ \mathrm{toList}\ (p^{k})\ x = (\mathrm{toList}\ p\ x).\mathrm{rotate}\ k.$$$$
Lean4
theorem toList_isRotated {f : Perm α} {x y : α} (h : SameCycle f x y) : toList f x ~r toList f y :=
by
by_cases hx : x ∈ f.support
· obtain ⟨_ | k, _, hy⟩ := h.exists_pow_eq_of_mem_support hx
· simp only [coe_one, id, pow_zero] at hy
simp [hy, IsRotated.refl]
use k.succ
rw [← toList_pow_apply_eq_rotate, hy]
· rw [toList_eq_nil_iff.mpr hx, isRotated_nil_iff', eq_comm, toList_eq_nil_iff]
rwa [← h.mem_support_iff]
