Miscellaneous results about determinant

In this file, we collect various formulas about determinant of matrices.

theorem Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin n) R) (hv : ∑ j : Fin (n + 1), M j = 0) (j₁ : Fin (n + 1)) (j₂ : Fin (n + 1)) : (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det

Let M be a (n+1) × n matrix whose row sums to zero. Then all the matrices obtained by deleting one row have the same determinant up to a sign.

theorem Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin (n + 1)) R) (hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0) (j₁ : Fin (n + 1)) (j₂ : Fin (n + 1)) : (M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

Let M be a (n+1) × n matrix whose column sums to zero. Then all the matrices obtained by deleting one column have the same determinant up to a sign.