English
If f is cycle-on s and a ∈ s, then for all n ∈ ℕ, (f^n)(a) = a iff n is a multiple of |s|.
Русский
Если f — цикл на s и a ∈ s, то для любого n ∈ ℕ, f^n(a) = a тогда и только тогда, когда n делит по |s|.
LaTeX
$$$\mathrm{IsCycleOn}(f,s) \land a \in s \Rightarrow (f^n)a = a \iff |s| \mid n$$$
Lean4
theorem pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {n : ℕ} : (f ^ n) a = a ↔ #s ∣ n :=
by
obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha
· rw [coe_singleton, isCycleOn_singleton] at hf
simpa using IsFixedPt.iterate hf n
classical
have h (x : s) : ¬f x = x := hf.apply_ne hs x.2
have := (hf.isCycle_subtypePerm hs).orderOf
simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach, mem_attach, imp_self,
implies_true, filter_true_of_mem, card_attach] at this
rw [← this, orderOf_dvd_iff_pow_eq_one,
(hf.isCycle_subtypePerm hs).pow_eq_one_iff' (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
simp [-coe_sort_coe]
