smul — Mathlib

English

In a NonAssocRing α and NonAssocRing β, if h is Antiperiodic f c, then f(x + n·c) = (−1)^n 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 smul [Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β] (h : Antiperiodic f c) (a : γ) :
    Antiperiodic (a • f) c := by simp_all

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