feat(LinearAlgebra/Matrix/SchurComplement): adding matrix determinant…

… lemma (#7086)

Co-authored-by: liuyf0188 <118104061+liuyf0188@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

@@ -444,14 +444,32 @@ theorem det_one_sub_mul_comm (A : Matrix m n α) (B : Matrix n m α) :
   rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]
 #align matrix.det_one_sub_mul_comm Matrix.det_one_sub_mul_comm
 
-/-- A special case of the **Matrix determinant lemma** for when `A = I`.
-
-TODO: show this more generally. -/
+/-- A special case of the **Matrix determinant lemma** for when `A = I`. -/
 theorem det_one_add_col_mul_row (u v : m → α) : det (1 + col u * row v) = 1 + v ⬝ᵥ u := by
   rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
     Matrix.row_mul_col_apply]
 #align matrix.det_one_add_col_mul_row Matrix.det_one_add_col_mul_row
 
+/-- The **Matrix determinant lemma**
+
+TODO: show the more general version without `hA : IsUnit A.det` as
+`(A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u`.
+-/
+theorem det_add_col_mul_row {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :
+    (A + col u * row v).det = A.det * (1 + row v * A⁻¹ * col u).det := by
+  nth_rewrite 1 [← Matrix.mul_one A]
+  rwa [← Matrix.mul_nonsing_inv_cancel_left A (col u * row v),
+    ←Matrix.mul_add, det_mul, ←Matrix.mul_assoc, det_one_add_mul_comm,
+    ←Matrix.mul_assoc]
+
+/-- A generalization of the **Matrix determinant lemma** -/
+theorem det_add_mul {A : Matrix m m α} (U : Matrix m n α)
+    (V : Matrix n m α) (hA : IsUnit A.det) :
+    (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det := by
+  nth_rewrite 1 [← Matrix.mul_one A]
+  rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ←Matrix.mul_add,
+    det_mul, ←Matrix.mul_assoc, det_one_add_mul_comm, ←Matrix.mul_assoc]
+
 end Det
 
 end CommRing