iterate_mod_apply — Mathlib

English

If x is periodic with periods m and n for f, then x is periodic with period gcd(m,n).

Русский

Если x периодичен с периодами m и n для f, то x периодичен с периодом gcd(m,n).

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f n x \to IsPeriodicPt f (m.gcd n) x$$$

Lean4

theorem iterate_mod_apply (h : IsPeriodicPt f n x) (m : ℕ) : f^[m % n] x = f^[m] x := by
  conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

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