English
Determinant expressed via a row-sum condition and a submatrix determinant with row and column removal.
Русский
Детерминант выражается через сумму по строке и детерминант подматрицы после удаления строки и столбца.
LaTeX
$$$\\det M = (-1)^{i_0+j_0} \\left(\\sum_j M_{i_0 j}\\right) \\det\\bigl(M_{\\text{succAbove } i_0 \\text{ succAbove } j_0}\\bigr)$$$
Lean4
/-- 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 submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' {n : ℕ} (M : Matrix (Fin n) (Fin (n + 1)) R)
(hv : ∀ i, ∑ j, M i j = 0) (j₁ j₂ : Fin (n + 1)) :
(M.submatrix id (Fin.succAbove j₁)).det = Int.negOnePow (j₁ - j₂) • (M.submatrix id (Fin.succAbove j₂)).det :=
by
rw [← det_transpose, transpose_submatrix,
submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det M.transpose ?_ j₁ j₂, ← det_transpose,
transpose_submatrix, transpose_transpose]
ext
simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]
