English
For a finite β and a cycle f, f^a = f^b holds iff there exists a moved point x with (f^a)x = (f^b)x and f x ≠ x.
Русский
Для цикла f в конечном β, равенство f^a = f^b имеет место тогда и только тогда, когда найдется перемещаемая точка x такая, что (f^a)x = (f^b)x и f(x) ≠ 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_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} :
f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x := by
classical
cases nonempty_fintype β
constructor
· intro h
obtain ⟨x, hx, -⟩ := id hf
exact ⟨x, hx, by simp [h]⟩
· rintro ⟨x, hx, hx'⟩
wlog hab : a ≤ b generalizing a b
· exact (this hx'.symm (le_of_not_ge hab)).symm
suffices f ^ (b - a) = 1 by
rw [pow_sub _ hab, mul_inv_eq_one] at this
rw [this]
rw [hf.pow_eq_one_iff]
by_cases hfa : (f ^ a) x ∈ f.support
· refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']
· have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
simp only [zpow_one, zpow_natCast] at h
rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
contradiction
