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 _ _ _