English
For any semiring R, scalar c acts on the Finsupp basis element by scaling the value: c • single a b = single a (c × b).
Русский
Для любого полукольца R скаляр действует на базисный элемент Finsupp, умножая значение: c • single a b = single a (c × b).
LaTeX
$$$[Semiring R] \\; (c : R) \\, (a : \\alpha) \\, (b : R) : c \\cdot \\mathrm{single}(a,b) = \\mathrm{single}(a, c \\cdot b)$$$
Lean4
theorem smul_single' {_ : Semiring R} (c : R) (a : α) (b : R) : c • Finsupp.single a b = Finsupp.single a (c * b) := by
simp