add_nat_mul_eq — Mathlib

English

If f is antiperiodic with period c, then for every natural n, f(x + n c) = (-1)^n f(x).

Русский

Если f антипериодична с периодом c, то для всякого натурального n выполняется f(x + n c) = (-1)^n f(x).

LaTeX

$$$f(x + n c) = (-1)^n f(x)$$$

Lean4

theorem add_nat_mul_eq [NonAssocSemiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : f (x + n * c) = (-1) ^ n * f x :=
  by simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg, Int.cast_one] using h.add_nsmul_eq n

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