Diagonal entries of the adjugate as principal minors

For a square matrix A indexed by an arbitrary finite type n, the diagonal entry adjugate A i i is the determinant of the principal submatrix of A obtained by deleting row and column i. The analogous statement for Fin n.succ, including the off-diagonal entries, is Matrix.adjugate_fin_succ_eq_det_submatrix; the version here needs no reindexing to Fin.

Main results

• Matrix.adjugate_apply_self_eq_det_submatrix: adjugate A i i is the determinant of A.submatrix (↑) (↑), where (↑) : {j // j ≠ i} → n.

theorem Matrix.adjugate_apply_self_eq_det_submatrix {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n R) (i : n) : A.adjugate i i = (A.submatrix Subtype.val Subtype.val).det

The diagonal entry adjugate A i i is the principal minor of A obtained by deleting row and column i. See Matrix.adjugate_fin_succ_eq_det_submatrix for all entries when the index type is Fin n.succ.