English
For a finite β and a cycle f, f^n = 1 iff there exists a moved point x with (f^n)x = x.
Русский
Для цикла f в конечном β, f^n = 1 тогда, когда существует перемещаемая точка x с (f^n)x = x.
LaTeX
$$$\\forall f : \\mathrm{Perm}(\\beta),\\; \\mathrm{IsCycle}(f) \\Rightarrow \\forall n:\\mathbb{N},\\; f^n = 1 \\iff \\exists x, f x \\neq x \\land (f^n)x = x.$$$
Lean4
theorem pow_eq_one_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} : f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x := by
classical
cases nonempty_fintype β
constructor
· intro h
obtain ⟨x, hx, -⟩ := id hf
exact ⟨x, hx, by simp [h]⟩
· rintro ⟨x, hx, hx'⟩
by_cases h : support (f ^ n) = support f
· rw [← mem_support, ← h, mem_support] at hx
contradiction
· rw [hf.support_pow_eq_iff, Classical.not_not] at h
obtain ⟨k, rfl⟩ := h
rw [pow_mul, pow_orderOf_eq_one, one_pow]
-- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption
