vecMul_sub — Mathlib

English

For any w ∈ α^m and v1,v2 ∈ α^n, vecMulVec w (v1 - v2) = vecMulVec w v1 - vecMulVec w v2. This is the componentwise linearity of vecMulVec.

Русский

Для вектора w и векторов v1, v2 выполняется vecMulVec w (v1 - v2) = vecMulVec w v1 - vecMulVec w v2.

LaTeX

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

Lean4

theorem vecMul_sub [Fintype m] (A B : Matrix m n α) (x : m → α) : x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B := by
  simp [sub_eq_add_neg, vecMul_add, vecMul_neg]

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