smul_single — Mathlib

English

Scalar multiplication distributes over the finsupp single operator: c • single a b = single a (c • b).

Русский

Скалярное умножение распределяется над оператором single: c • single a b = single a (c • b).

LaTeX

$$$[Zero M][SMulZeroClass R M](c : R)(a : \\alpha)(b : M) : c \\cdot \\mathrm{single}(a,b) = \\mathrm{single}(a, c \\cdot b)$$$

Lean4

@[simp]
theorem smul_single [Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) :
    c • Finsupp.single a b = Finsupp.single a (c • b) :=
  mapRange_single

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