sub_mulVec — Mathlib

English

For any w ∈ α^m and v1,v2 ∈ α^n, vecMul w (v1 - v2) = vecMul w v1 - vecMul w v2. This expresses linearity in the right argument.

Русский

Для вектора w и векторов 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_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) : (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x := by
  simp [sub_eq_add_neg, add_mulVec, neg_mulVec]

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