zpow_apply_eq_zpow_apply — Mathlib

English

Let s be a finite set and f a cycle-on s. Then for a ∈ s and integers m,n, (f^m)a = (f^n)a iff m ≡ n (mod |s|).

Русский

Пусть s конечное множество, f — цикл на s. Тогда для a ∈ s и целых m,n выполняется (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 zpow_apply_eq_zpow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {m n : ℤ} :
    (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD #s] :=
  by
  rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]

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