smul_apply — Mathlib

English

Scalar multiplication acts componentwise on the direct sum: (b • v)_i = b • v_i for all i.

Русский

Умножение на скаляр действует по координатам на прямой сумме: (b • v)_i = b • v_i для всех i.

LaTeX

$$$\\forall b\\in R,\\; \\forall v\\in \\bigoplus_{i} M_i,\\; (b\\cdot v)_i = b\\cdot v_i.$$$

Lean4

theorem smul_apply (b : R) (v : ⨁ i, M i) (i : ι) : (b • v) i = b • v i :=
  DFinsupp.smul_apply _ _ _

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