sub_vecMulVec — Mathlib

English

For any w ∈ α^m and v1,v2 ∈ α^n, vecMulVec (w1 - w2) v = vecMulVec w1 v - vecMulVec w2 v. This is the linearity of vecMulVec in the left vector argument.

Русский

Для векторов w1, w2 ∈ α^m и v ∈ α^n: vecMulVec (w1 - w2) v = vecMulVec w1 v - vecMulVec w2 v.

LaTeX

$$$ vecMulVec (w1 - w2) v = vecMulVec w1 v - vecMulVec w2 v $$$

Lean4

theorem sub_vecMulVec (w₁ w₂ : m → α) (v : n → α) : vecMulVec (w₁ - w₂) v = vecMulVec w₁ v - vecMulVec w₂ v :=
  ext fun _ _ => sub_mul _ _ _

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