feat(linear_algebra/matrix/adjugate): add `det_eq_sum_mul_adjugate_ro…

…w` (#19117)

From lean-matrix-cookbook

src/data/matrix/notation.lean

@@ -314,6 +314,18 @@ empty_eq _
   submatrix A (vec_cons i row) col = vec_cons (λ j, A i (col j)) (submatrix A row col) :=
 by { ext i j, refine fin.cases _ _ i; simp [submatrix] }
 
+/-- Updating a row then removing it is the same as removing it. -/
+@[simp] lemma submatrix_update_row_succ_above (A : matrix (fin m.succ) n' α)
+  (v : n' → α) (f : o' → n') (i : fin m.succ) :
+  (A.update_row i v).submatrix i.succ_above f = A.submatrix i.succ_above f :=
+ext $ λ r s, (congr_fun (update_row_ne (fin.succ_above_ne i r) : _ = A _) (f s) : _)
+
+/-- Updating a column then removing it is the same as removing it. -/
+@[simp] lemma submatrix_update_column_succ_above (A : matrix m' (fin n.succ) α)
+  (v : m' → α) (f : o' → m') (i : fin n.succ) :
+  (A.update_column i v).submatrix f i.succ_above = A.submatrix f i.succ_above :=
+ext $ λ r s, update_column_ne (fin.succ_above_ne i s)
+
 end submatrix
 
 section vec2_and_vec3

src/linear_algebra/matrix/adjugate.lean

@@ -340,7 +340,6 @@ lemma _root_.alg_hom.map_adjugate {R A B : Type*} [comm_semiring R] [comm_ring A
   (M : matrix n n A) : f.map_matrix M.adjugate = matrix.adjugate (f.map_matrix M) :=
 f.to_ring_hom.map_adjugate _
 
-
 lemma det_adjugate (A : matrix n n α) : (adjugate A).det = A.det ^ (fintype.card n - 1) :=
 begin
   -- get rid of the `- 1`
@@ -387,6 +386,33 @@ end
   adjugate !![a, b; c, d] = !![d, -b; -c, a] :=
 adjugate_fin_two _
 
+lemma adjugate_fin_succ_eq_det_submatrix {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) α) (i j) :
+  adjugate A i j = (-1)^(j + i : ℕ) * det (A.submatrix j.succ_above i.succ_above) :=
+begin
+  simp_rw [adjugate_apply, det_succ_row _ j, update_row_self, submatrix_update_row_succ_above],
+  rw [fintype.sum_eq_single i (λ h hjk, _), pi.single_eq_same, mul_one],
+  rw [pi.single_eq_of_ne hjk, mul_zero, zero_mul],
+end
+
+lemma det_eq_sum_mul_adjugate_row (A : matrix n n α) (i : n) :
+  det A = ∑ j : n, A i j * adjugate A j i :=
+begin
+  haveI : nonempty n := ⟨i⟩,
+  obtain ⟨n', hn'⟩ := nat.exists_eq_succ_of_ne_zero (fintype.card_ne_zero : fintype.card n ≠ 0),
+  obtain ⟨e⟩ := fintype.trunc_equiv_fin_of_card_eq hn',
+  let A' := reindex e e A,
+  suffices : det A' = ∑ j : fin n'.succ, A' (e i) j * adjugate A' j (e i),
+  { simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ←e.sum_comp,
+      equiv.symm_apply_apply] at this,
+    exact this },
+  rw det_succ_row A' (e i),
+  simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ←adjugate_fin_succ_eq_det_submatrix],
+end
+
+lemma det_eq_sum_mul_adjugate_col (A : matrix n n α) (j : n) :
+  det A = ∑ i : n, A i j * adjugate A j i :=
+by simpa only [det_transpose, ←adjugate_transpose] using det_eq_sum_mul_adjugate_row Aᵀ j
+
 lemma adjugate_conj_transpose [star_ring α] (A : matrix n n α) : A.adjugateᴴ = adjugate (Aᴴ) :=
 begin
   dsimp only [conj_transpose],