From 39b61a6aaa6327f75e5d27b5320e2fc4856303ca Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 30 Sep 2024 08:52:11 +0000 Subject: [PATCH] chore(Data/Matrix): some trivial lemmas about `row` and `col` (#17243) Co-authored-by: Eric Wieser --- Mathlib/Data/Matrix/RowCol.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Data/Matrix/RowCol.lean b/Mathlib/Data/Matrix/RowCol.lean index 2529d88fd19ee..6ce7feb0bcaa5 100644 --- 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 :=