vecMulVec_sub — Mathlib

English

For any m→α and v1,v2: vecMulVec w (v1 - v2) = vecMulVec w v1 - vecMulVec w v2. This expresses linearity in the right argument.

Русский

Для w : m→α и v1,v2 : n→α верно: vecMulVec w (v1 - v2) = vecMulVec w v1 - vecMulVec w v2.

LaTeX

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

Lean4

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

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