map_mod_nat — Mathlib

English

If f is periodic with period a, then f(n mod a) = f(n) for all n.

Русский

Если f периодична с периодом a, тогда для всех n выполняется f(n mod a) = f(n).

LaTeX

$$$ \forall n, f(n \bmod a) = f(n) $$$

Lean4

theorem _root_.Function.Periodic.map_mod_nat {α : Type*} {f : ℕ → α} {a : ℕ} (hf : Periodic f a) :
    ∀ n, f (n % a) = f n := fun n => by conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

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