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₁ 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₁ 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.

theorem Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_det {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1)) (hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0) : M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Let M be a (n+1) × (n+1) matrix. Assume that all columns, but the j₀-column, sums to zero. Then its determinant is, up to sign, the sum of the j₀-column times the determinant of the matrix obtained by deleting any row and the j₀-column.

theorem Matrix.det_eq_sum_row_mul_submatrix_succAbove_succAbove_det {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1)) (hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j : Fin (n + 1), M i j = 0) : M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ j : Fin (n + 1), M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Let M be a (n+1) × (n+1) matrix. Assume that all rows, but the i₀-row, sums to zero. Then its determinant is, up to sign, the sum of the i₀-row times the determinant of the matrix obtained by deleting the i₀-row and any column.