int_mul_sub_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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