English
For a finite β and a cycle f, f^a = f^b holds exactly when there exists a moved point x with (f^a)x = (f^b)x and f x ≠ x.
Русский
Для цикла f в конечном β равенство f^a = f^b происходит тогда, когда существует точка x, которую f двигает, и (f^a)x = (f^b)x.
LaTeX
$$$\\forall f : \\mathrm{Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\Rightarrow \\forall a,b:\\mathbb{N},\\; f^a = f^b \\iff \\exists x, f x \\neq x \\land (f^a)x = (f^b)x.$$$
Lean4
theorem pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : IsCycle (f ^ n) ↔ n.Coprime (orderOf f) := by
classical
cases nonempty_fintype β
constructor
· intro h
have hr : support (f ^ n) = support f := by
rw [hf.support_pow_eq_iff]
rintro ⟨k, rfl⟩
refine h.ne_one ?_
simp [pow_mul, pow_orderOf_eq_one]
have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
rw [orderOf_pow, Nat.div_eq_self] at this
rcases this with h | _
· exact absurd h (orderOf_pos _).ne'
· rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
· intro h
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
refine hf'.of_pow fun x hx => ?_
rw [hm]
exact support_pow_le _ n hx
