chore(Data/Matrix): some trivial lemmas about row and col (#17243)

Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Sep 30, 2024 · 39b61a6 · 39b61a6
1 parent eed3300
commit 39b61a6
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/Mathlib/Data/Matrix/RowCol.lean b/Mathlib/Data/Matrix/RowCol.lean
@@ -136,6 +136,16 @@ theorem row_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α
   ext
   rfl
 
+theorem row_mulVec_eq_const [Fintype m] [NonUnitalNonAssocSemiring α]  (v w : m → α) :
+    Matrix.row ι v *ᵥ w = Function.const _ (v ⬝ᵥ w) := rfl
+
+theorem mulVec_col_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
+    v ᵥ* Matrix.col ι w = Function.const _ (v ⬝ᵥ w) := rfl
+
+theorem row_mul_col [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) :
+    row ι v * col ι w = of fun _ _ => v ⬝ᵥ w :=
+  rfl
+
 @[simp]
 theorem row_mul_col_apply [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) (i j) :
     (row ι v * col ι w) i j = v ⬝ᵥ w :=