feat(data/matrix): Lemmas about vec_mul, mul_vec, dot_product, …

…`inv` (#14644)

src/data/matrix/basic.lean

@@ -389,7 +389,7 @@ end diag
 
 section dot_product
 
-variable [fintype m]
+variables [fintype m] [fintype n]
 
 /-- `dot_product v w` is the sum of the entrywise products `v i * w i` -/
 def dot_product [has_mul α] [add_comm_monoid α] (v w : m → α) : α :=
@@ -399,7 +399,7 @@ def dot_product [has_mul α] [add_comm_monoid α] (v w : m → α) : α :=
    so that `r₁ • a ⬝ᵥ r₂ • b` is parsed as `(r₁ • a) ⬝ᵥ (r₂ • b)` here. -/
 localized "infix  ` ⬝ᵥ `:72 := matrix.dot_product" in matrix
 
-lemma dot_product_assoc [fintype n] [non_unital_semiring α] (u : m → α) (w : n → α)
+lemma dot_product_assoc [non_unital_semiring α] (u : m → α) (w : n → α)
   (v : matrix m n α) :
   (λ j, u ⬝ᵥ (λ i, v i j)) ⬝ᵥ w = u ⬝ᵥ (λ i, (v i) ⬝ᵥ w) :=
 by simpa [dot_product, finset.mul_sum, finset.sum_mul, mul_assoc] using finset.sum_comm
@@ -413,7 +413,7 @@ by simp_rw [dot_product, mul_comm]
 by simp [dot_product]
 
 section non_unital_non_assoc_semiring
-variables [non_unital_non_assoc_semiring α] (u v w : m → α)
+variables [non_unital_non_assoc_semiring α] (u v w : m → α) (x y : n → α)
 
 @[simp] lemma dot_product_zero : v ⬝ᵥ 0 = 0 := by simp [dot_product]
 
@@ -429,6 +429,10 @@ by simp [dot_product, add_mul, finset.sum_add_distrib]
 @[simp] lemma dot_product_add : u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w :=
 by simp [dot_product, mul_add, finset.sum_add_distrib]
 
+@[simp] lemma sum_elim_dot_product_sum_elim :
+  (sum.elim u x) ⬝ᵥ (sum.elim v y) = u ⬝ᵥ v + x ⬝ᵥ y :=
+by simp [dot_product]
+
 end non_unital_non_assoc_semiring
 
 section non_unital_non_assoc_semiring_decidable
@@ -1229,6 +1233,14 @@ by { ext, apply neg_dot_product }
 lemma mul_vec_neg [fintype n] (v : n → α) (A : matrix m n α) : mul_vec A (-v) = - mul_vec A v :=
 by { ext, apply dot_product_neg }
 
+lemma sub_mul_vec [fintype n] (A B : matrix m n α) (x : n → α) :
+  mul_vec (A - B) x = mul_vec A x - mul_vec B x :=
+by simp [sub_eq_add_neg, add_mul_vec, neg_mul_vec]
+
+lemma vec_mul_sub [fintype m] (A B : matrix m n α) (x : m → α) :
+  vec_mul x (A - B) = vec_mul x A - vec_mul x B :=
+by simp [sub_eq_add_neg, vec_mul_add, vec_mul_neg]
+
 end non_unital_non_assoc_ring
 
 section non_unital_comm_semiring
@@ -1243,6 +1255,14 @@ lemma vec_mul_transpose [fintype n] (A : matrix m n α) (x : n → α) :
   vec_mul x Aᵀ = mul_vec A x :=
 by { ext, apply dot_product_comm }
 
+lemma mul_vec_vec_mul [fintype n] [fintype o] (A : matrix m n α) (B : matrix o n α) (x : o → α) :
+  mul_vec A (vec_mul x B) = mul_vec (A ⬝ Bᵀ) x :=
+by rw [← mul_vec_mul_vec, mul_vec_transpose]
+
+lemma vec_mul_mul_vec [fintype m] [fintype n] (A : matrix m n α) (B : matrix m o α) (x : n → α) :
+  vec_mul (mul_vec A x) B = vec_mul x (Aᵀ ⬝ B) :=
+by rw [← vec_mul_vec_mul, vec_mul_transpose]
+
 end non_unital_comm_semiring
 
 section comm_semiring

src/data/matrix/block.lean

@@ -190,6 +190,20 @@ begin
     pi.add_apply],
 end
 
+lemma from_blocks_mul_vec [fintype l] [fintype m] [non_unital_non_assoc_semiring α]
+  (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) (x : l ⊕ m → α) :
+  mul_vec (from_blocks A B C D) x =
+  sum.elim (mul_vec A (x ∘ sum.inl) + mul_vec B (x ∘ sum.inr))
+           (mul_vec C (x ∘ sum.inl) + mul_vec D (x ∘ sum.inr)) :=
+by { ext i, cases i; simp [mul_vec, dot_product] }
+
+lemma vec_mul_from_blocks [fintype n] [fintype o] [non_unital_non_assoc_semiring α]
+  (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) (x : n ⊕ o → α) :
+  vec_mul x (from_blocks A B C D) =
+  sum.elim (vec_mul (x ∘ sum.inl) A + vec_mul (x ∘ sum.inr) C)
+           (vec_mul (x ∘ sum.inl) B + vec_mul (x ∘ sum.inr) D) :=
+by { ext i, cases i; simp [vec_mul, dot_product] }
+
 variables [decidable_eq l] [decidable_eq m]
 
 @[simp] lemma from_blocks_diagonal [has_zero α] (d₁ : l → α) (d₂ : m → α) :

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -178,7 +178,7 @@ lemma det_ne_zero_of_right_inverse [nontrivial α] (h : A ⬝ B = 1) : A.det ≠
 
 end invertible
 
-variables [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α]
+variables [fintype n] [decidable_eq n] [comm_ring α]
 variables (A : matrix n n α) (B : matrix n n α)
 
 lemma is_unit_det_transpose (h : is_unit A.det) : is_unit Aᵀ.det :=
@@ -246,12 +246,44 @@ begin
   rw [←inv_of_eq_nonsing_inv, matrix.inv_of_mul_self],
 end
 
+@[simp] lemma mul_nonsing_inv_cancel_right (B : matrix m n α) (h : is_unit A.det) :
+  B ⬝ A ⬝ A⁻¹ = B :=
+by simp [matrix.mul_assoc, mul_nonsing_inv A h]
+
+@[simp] lemma mul_nonsing_inv_cancel_left (B : matrix n m α) (h : is_unit A.det) :
+  A ⬝ (A⁻¹ ⬝ B) = B :=
+by simp [←matrix.mul_assoc, mul_nonsing_inv A h]
+
+@[simp] lemma nonsing_inv_mul_cancel_right (B : matrix m n α) (h : is_unit A.det) :
+  B ⬝ A⁻¹ ⬝ A = B :=
+by simp [matrix.mul_assoc, nonsing_inv_mul A h]
+
+@[simp] lemma nonsing_inv_mul_cancel_left (B : matrix n m α) (h : is_unit A.det) :
+  A⁻¹ ⬝ (A ⬝ B) = B :=
+by simp [←matrix.mul_assoc, nonsing_inv_mul A h]
+
 @[simp] lemma mul_inv_of_invertible [invertible A] : A ⬝ A⁻¹ = 1 :=
 mul_nonsing_inv A (is_unit_det_of_invertible A)
 
 @[simp] lemma inv_mul_of_invertible [invertible A] : A⁻¹ ⬝ A = 1 :=
 nonsing_inv_mul A (is_unit_det_of_invertible A)
 
+@[simp] lemma mul_inv_cancel_right_of_invertible (B : matrix m n α) [invertible A] :
+  B ⬝ A ⬝ A⁻¹ = B :=
+mul_nonsing_inv_cancel_right A B (is_unit_det_of_invertible A)
+
+@[simp] lemma mul_inv_cancel_left_of_invertible (B : matrix n m α) [invertible A] :
+  A ⬝ (A⁻¹ ⬝ B) = B :=
+mul_nonsing_inv_cancel_left A B (is_unit_det_of_invertible A)
+
+@[simp] lemma inv_mul_cancel_right_of_invertible (B : matrix m n α) [invertible A] :
+  B ⬝ A⁻¹ ⬝ A = B :=
+nonsing_inv_mul_cancel_right A B (is_unit_det_of_invertible A)
+
+@[simp] lemma inv_mul_cancel_left_of_invertible (B : matrix n m α) [invertible A] :
+  A⁻¹ ⬝ (A ⬝ B) = B :=
+nonsing_inv_mul_cancel_left A B (is_unit_det_of_invertible A)
+
 lemma nonsing_inv_cancel_or_zero :
   (A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1) ∨ A⁻¹ = 0 :=
 begin
@@ -464,6 +496,9 @@ by rw [← (A⁻¹).transpose_transpose, vec_mul_transpose, transpose_nonsing_in
 
 /-! ### More results about determinants -/
 
+section det
+variables [fintype m] [decidable_eq m]
+
 /-- A variant of `matrix.det_units_conj`. -/
 lemma det_conj {M : matrix m m α} (h : is_unit M) (N : matrix m m α) :
   det (M ⬝ N ⬝ M⁻¹) = det N :=
@@ -537,4 +572,6 @@ lemma det_one_add_col_mul_row (u v : m → α) : det (1 + col u ⬝ row v) = 1 +
 by rw [det_one_add_mul_comm, det_unique, pi.add_apply, pi.add_apply, matrix.one_apply_eq,
        matrix.row_mul_col_apply]
 
+end det
+
 end matrix