English
For a finite β and a cycle f, f^a = f^b 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{Equiv.Perm}(\\beta),\\; f^{\\text{IsCycle}} \\Rightarrow \\forall a,b,\\; f^a = f^b \\iff \\exists x, f x \\neq x \\land (f^a)x = (f^b)x.$$$
Lean4
theorem isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf : IsCycle f) (hf' : (orderOf f).Prime) (n : ℕ)
(hn : 0 < n) (hn' : n < orderOf f) : IsCycle (f ^ n) := by
classical
cases nonempty_fintype β
have : n.Coprime (orderOf f) := by
refine Nat.Coprime.symm ?_
rw [Nat.Prime.coprime_iff_not_dvd hf']
exact Nat.not_dvd_of_pos_of_lt hn hn'
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
have hf'' := hf
rw [← hm] at hf''
refine hf''.of_pow ?_
rw [hm]
exact support_pow_le f n
