zsmul_sub_eq — Mathlib

English

For AddCommGroup α and SubtractionMonoid β, if f is Antiperiodic with c, then f(n•c - x) = (n.negOnePow)•f(-x) for all integers n.

Русский

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

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \forall x, \forall n\in\mathbb{Z}, \ f(n\cdot c - x) = (n.negOnePow)\cdot f(-x)$$$

Lean4

theorem zsmul_sub_eq [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) :
    f (n • c - x) = (n.negOnePow : ℤ) • f (-x) :=
  by
  rw [sub_eq_add_neg, add_comm]
  exact h.add_zsmul_eq n

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