English
For any g with fixed x, the equality of powers on x is governed by the cycle length.
Русский
Для любой g с фиксированной x равенство значений степеней на x задаётся длиной цикла.
LaTeX
$$$(g x = x) \\Rightarrow (g^m) x = (g^n) x \\iff m \\equiv n (mod |cycleOf x|$)$$
Lean4
theorem exists_pow_eq [DecidableEq α] [Fintype α] (f : Perm α) (h : SameCycle f x y) :
∃ i : ℕ, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y :=
by
by_cases hx : x ∈ f.support
· obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
rcases k with - | k
· refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
simp only [pow_zero, coe_one, id_eq] at hk'
subst hk'
rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self, pow_orderOf_eq_one, one_apply]
· exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
· refine ⟨1, zero_lt_one, by simp, ?_⟩
obtain ⟨k, rfl⟩ := h
rw [notMem_support] at hx
rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
