sub_nat_mul_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sub_nat_mul_eq [NonAssocRing α] [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.sub_nsmul_eq n

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