sub_vecMul — Mathlib

English

For any w ∈ α^m and v1, v2 ∈ α^n, vecMul w (v1 - v2) = vecMul w v1 - vecMul w v2. This is the same linearity as in vecMul and vecMulVec with left argument w.

Русский

Для w ∈ α^m и векторов v1, v2 выполняется vecMul w (v1 - v2) = vecMul w v1 - vecMul w v2.

LaTeX

$$$ vecMul w (v1 - v2) = vecMul w v1 - vecMul w v2 $$$

Lean4

theorem sub_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) : (x - y) ᵥ* A = x ᵥ* A - y ᵥ* A :=
  by
  ext
  apply sub_dotProduct

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