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