neg_mulVec — Mathlib

English

Let α be a (nonunital, nonassociative) ring. For any finite n, any vector v ∈ α^n and any matrix A ∈ α^{m×n}, we have (-A) *ᵥ v = -(A *ᵥ v). That is, negation distributes over the vecMul on the left.

Русский

Пусть α — кольцо без единицы, неассоциативное. Для любой размерности n, вектора v ∈ α^n и матрицы A ∈ α^{m×n} выполняется (-A) *ᵥ v = -(A *ᵥ v). То есть отрицание матрицы распространяется на левое умножение на вектор.

LaTeX

$$$(-A) *ᵥ v = -(A *ᵥ v)$$$

Lean4

theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = -(A *ᵥ v) :=
  by
  ext
  apply neg_dotProduct

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