English
Let α be a (nonunital, nonassociative) ring. For every finite index set m, every n, and all v ∈ α^m, A ∈ α^{m×n}, we have (-v)ᵥ* (-A) = vᵥ* A. In words, the vecMul operation is bilinear with respect to negation of both arguments.
Русский
Пусть α — кольцо без единицы, неассоциативное. Для любых конечных множеств m, n и векторов v ∈ α^m, матрицы A ∈ α^{m×n} выполняется (-v)ᵥ* (-A) = vᵥ* A. Другими словами, операция vecMul билинейна по отношению к отрицанию обоих аргументов.
LaTeX
$$$(-v) ᵥ* (-A) = v ᵥ* A$$$
Lean4
theorem neg_vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* (-A) = v ᵥ* A := by
rw [vecMul_neg, neg_vecMul, neg_neg]
