zpow_apply_eq — Mathlib

English

For all a ∈ s, (f^n)(a) = a iff n ≡ 0 mod |s| in the integer setting, so the z-powers share the same fixed points pattern as natural powers with modulus |s|.

Русский

Для всех a ∈ s, (f^n)(a) = a тогда и только тогда, когда n ≡ 0 (mod |s|) в целочисленном контексте.

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \land a\in s \Rightarrow (f^n)a = a \iff (|s|) \mid n \text{ in } \mathbb{Z}$$$

Lean4

theorem zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) : ∀ {n : ℤ}, (f ^ n) a = a ↔ (#s : ℤ) ∣ n
  | Int.ofNat _ => (hf.pow_apply_eq ha).trans Int.natCast_dvd_natCast.symm
  | Int.negSucc n => by
    rw [zpow_negSucc, ← inv_pow]
    exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Похожие утверждения