neg_nsmul — Mathlib

English

If f is c-periodic, then f is (−n·c)-periodic for natural n, i.e., the negated multiple of the period is a period.

Русский

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

LaTeX

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

Lean4

theorem neg_nsmul [AddGroup α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n • c)) :=
  (h.nsmul n).neg

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