add_int_mul_eq — Mathlib

English

In a 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) для всех целых n.

LaTeX

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

Lean4

theorem add_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.add_zsmul_eq n

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