sub_nsmul_eq — Mathlib

English

For AddGroup α and SubtractionMonoid β, if f is Antiperiodic with c, then for natural n we have f(x − n•c) = (-1)^n f(-x).

Русский

Для AddGroup α и SubtractionMonoid β, если f антипериодическая с c, тогда при любом натуральном n выполняется f(x − n•c) = (-1)^n f(-x).

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \forall n \in \mathbb{N}, \ f(x - n\cdot c) = (-1)^n \cdot f(-x)$$$

Lean4

theorem sub_nsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) :
    f (x - n • c) = (-1) ^ n • f x := by simpa only [Int.reduceNeg, natCast_zsmul] using h.sub_zsmul_eq n

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