nsmul_sub_eq — Mathlib

English

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

Русский

Для AddCommGroup α и SubtractionMonoid β, если f антипериодическая с c, то f((n)•c − x) = (-1)^n f(-x).

LaTeX

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

Lean4

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

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