pow_apply_eq_pow_apply — Mathlib

English

For a cycle-on s and a ∈ s, (f^m)(a) = (f^n)(a) iff m ≡ n (mod |s|).

Русский

Если f — цикл на s и a ∈ s, то (f^m)(a) = (f^n)(a) тогда и только тогда, когда m ≡ n (mod |s|).

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \land a\in s \Rightarrow (f^m)a = (f^n)a \iff m \equiv n \pmod{|s|}$$$

Lean4

theorem pow_apply_eq_pow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {m n : ℕ} :
    (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s] :=
  by
  rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

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