mulVec_sub — Mathlib

English

For any matrix A ∈ α^{m×n} and vectors x,y ∈ α^n, A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y. This is the standard linearity of vecMul in the vector argument.

Русский

Для матрицы A и векторов x,y выполняется A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y.

LaTeX

$$$A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y$$$

Lean4

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

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