From b762514e5ea671810f8662491bdf4395ada67238 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= <martin.dvorak@matfyz.cz>
Date: Thu, 16 May 2024 19:48:07 +0000
Subject: [PATCH] feat (Data/Matrix/Basic): `Matrix` versions of `neg_mul_neg`
 (#12901)

---
 Mathlib/Data/Matrix/Basic.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
index d4679dbcaaabe..85dfcae2b79e5 100644
--- a/Mathlib/Data/Matrix/Basic.lean
+++ b/Mathlib/Data/Matrix/Basic.lean
@@ -902,6 +902,9 @@ theorem neg_dotProduct : -v ⬝ᵥ w = -(v ⬝ᵥ w) := by simp [dotProduct]
 theorem dotProduct_neg : v ⬝ᵥ -w = -(v ⬝ᵥ w) := by simp [dotProduct]
 #align matrix.dot_product_neg Matrix.dotProduct_neg
 
+lemma neg_dotProduct_neg : -v ⬝ᵥ -w = v ⬝ᵥ w := by
+  rw [neg_dotProduct, dotProduct_neg, neg_neg]
+
 @[simp]
 theorem sub_dotProduct : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w := by simp [sub_eq_add_neg]
 #align matrix.sub_dot_product Matrix.sub_dotProduct
@@ -1944,6 +1947,9 @@ theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A)
   apply dotProduct_neg
 #align matrix.vec_mul_neg Matrix.vecMul_neg
 
+lemma neg_vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* (-A) = v ᵥ* A := by
+  rw [vecMul_neg, neg_vecMul, neg_neg]
+
 theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = - (A *ᵥ v) := by
   ext
   apply neg_dotProduct
@@ -1954,6 +1960,9 @@ theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v)
   apply dotProduct_neg
 #align matrix.mul_vec_neg Matrix.mulVec_neg
 
+lemma neg_mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ (-v) = A *ᵥ v := by
+  rw [mulVec_neg, neg_mulVec, neg_neg]
+
 theorem mulVec_sub [Fintype n] (A : Matrix m n α) (x y : n → α) :
     A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y := by
   ext