smul_single' — Mathlib

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

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