sub_int_mul_eq — Mathlib

English

For NonAssocRing α and NonAssocRing β, if f is Antiperiodic with c, then f(x − n·c) = (n.negOnePow)·f x for all integers n.

Русский

Для неассоциированного кольца α и β, если f антипериодическая с c, то f(x − n·c) = (-1)^n f(x).

LaTeX

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

Lean4

theorem sub_int_mul_eq [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) :
    f (x - n * c) = (n.negOnePow : ℤ) * f x := by simpa only [zsmul_eq_mul] using h.sub_zsmul_eq n

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