sub_zsmul_eq — Mathlib

English

For AddGroup α, SubtractionMonoid β, if f is antiperiodic with c, then f(x − n•c) = (n.negOnePow)•f x for all integers n.

Русский

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

LaTeX

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

Lean4

theorem sub_zsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) :
    f (x - n • c) = (n.negOnePow : ℤ) • f x := by
  simpa only [sub_eq_add_neg, neg_zsmul, Int.negOnePow_neg] using h.add_zsmul_eq (-n)

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