English
Let a,b ∈ s. If f is cycle-on s, there exists n < |s| such that (f^n) a = b.
Русский
Пусть a,b ∈ s. Если f — цикл на s, тогда существует n < |s| such, что (f^n) a = b.
LaTeX
$$$\mathrm{IsCycleOn}(f,s) \land a\in s \land b\in s \Rightarrow \exists n < |s|, (f^n)a = b$$$
Lean4
theorem exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) : ∃ n < #s, (f ^ n) a = b := by
classical
obtain ⟨n, rfl⟩ := hf.2 ha hb
obtain ⟨k, hk⟩ := (Int.mod_modEq n #s).symm.dvd
refine ⟨n.natMod #s, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', ?_⟩
rw [← zpow_natCast, Int.natMod,
Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2 (Nonempty.card_pos ⟨a, ha⟩).ne'),
sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
simp only [zpow_natCast, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
