smul_vecMul — Mathlib

English

The product commutes with scalar action on the left: (b • v) ᵥ* M = b • (v ᵥ* M).

Русский

Произведение вектора и матрицы коммутирует со скалярным действует слева: (b • v) ᵥ* M = b • (v ᵥ* M).

LaTeX

$$$ (b \cdot v) ᵥ* M = b \cdot (v ᵥ* M) $$$

Lean4

theorem smul_vecMul [Fintype m] [DistribSMul R α] [IsScalarTower R α α] (b : R) (v : m → α) (M : Matrix m n α) :
    (b • v) ᵥ* M = b • v ᵥ* M := by
  ext
  exact smul_dotProduct _ _ _

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