neg_mulVec_neg — Mathlib

English

In a nonunital, nonassociative setting with finite index, (-A) *ᵥ (-v) = A *ᵥ v. Negating both the matrix and the vector preserves the vecMul result.

Русский

В условиях без единицы и неассоциативности: (-A) *ᵥ (-v) = A *ᵥ v. Отрицание обеих частей не меняет результат vecMul.

LaTeX

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

Lean4

theorem neg_mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ (-v) = A *ᵥ v := by
  rw [mulVec_neg, neg_mulVec, neg_neg]

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