English
In a nonunital, nonassociative ring, the vecMul is additive in the vector argument: A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y for A ∈ α^{m×n}, x,y ∈ α^n.
Русский
В кольце без единицы, неассоциативном векторно-матричное умножение линейно по вектору: A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y.
LaTeX
$$$A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y$$$
Lean4
theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v) = -(A *ᵥ v) :=
by
ext
apply dotProduct_neg