zsmul — Mathlib

English

If f is c-periodic, then f(n·c − x) = f(−x) for natural n.

Русский

Если f периодична по c, то f(n·c − x) = f(−x) для натурального n.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ ∀ n:\\mathbb{N}, f(n\\cdot c - x) = f(-x)$$$

Lean4

protected theorem zsmul [AddGroup α] (h : Periodic f c) (n : ℤ) : Periodic f (n • c) :=
  by
  rcases n with n | n
  · simpa only [Int.ofNat_eq_coe, natCast_zsmul] using h.nsmul n
  · simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

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