smul_single — Mathlib

English

Multiplying a basis element by a scalar a yields the basis element with the scaled coefficient: a • single m r = single m (a • r).

Русский

Умножение базисного элемента на скаляр даёт базисный элемент с масштабированным коэффициентом: a • single m r = single m (a • r).

LaTeX

$$$ a \\cdot \\mathrm{single}(m,r) = \\mathrm{single}(m, a \\cdot r) $$$

Lean4

@[to_additive (attr := simp) (dont_translate := A) smul_single]
theorem smul_single (a : A) (m : M) (r : R) : a • single m r = single m (a • r) := by ext;
  simp [single, ← Finsupp.smul_single]

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