mulVec_smul — Mathlib

English

Scaling the vector argument scales the matrix-vector product: M *ᵥ (b • v) = b • (M *ᵥ v).

Русский

Умножение вектора на скаляр масштабирует произведение: M *ᵥ (b • v) = b • (M *ᵥ v).

LaTeX

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

Lean4

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

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