smul_mulVec — Mathlib

English

The relation between scalar acting on M and the product with v: (b • M) *ᵥ v = b • (M *ᵥ v).

Русский

Связь между скаляром, действующим на матрицу, и произведением на вектор: (b • M) *ᵥ v = b • (M *ᵥ v).

LaTeX

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

Lean4

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

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