instNatSMul — Mathlib

English

There is a natural-number scalar action on finitely supported functions f : ι →₀ M given by (n • f)(i) = n • f(i) for all i.

Русский

Существует скалярное действие натуральных чисел на функции с конечной опорой f : ι →₀ M, задаваемое формулой (n • f)(i) = n • f(i) для всех i.

LaTeX

$$$\forall n \in \mathbb{N}, \forall f: \iota \to_0 M,\ (n \cdot f)(i) = n \cdot f(i) \quad \text{для всех } i.$$$

Lean4

/-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℕ` is not distributive
unless `F i`'s addition is commutative. -/
instance instNatSMul : SMul ℕ (ι →₀ M) where smul n v := v.mapRange (n • ·) (nsmul_zero _)

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