English
Determinant equality under row-sum pattern leading to a submatrix determinant with a sign.
Русский
Детерминант сохраняется при сумме строк с образованием подматрицы и знаком.
LaTeX
$$$\\det M = (-1)^{i_0+j_0} \\left(\\sum_j M_{i_0 j}\\right) \\det\\bigl(M_{\\text{submatrix } (\\operatorname{succAbove} i_0) (\\operatorname{succAbove} j_0)}\\bigr)$$$
Lean4
/-- 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. -/
theorem det_eq_sum_row_mul_submatrix_succAbove_succAbove_det {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R)
(i₀ j₀ : Fin (n + 1)) (hv : ∀ i ≠ i₀, ∑ j, M i j = 0) :
M.det = (-1) ^ (i₀ + j₀ : ℕ) * (∑ j, M i₀ j) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det :=
by
rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀ (by simpa using hv), ←
det_transpose, transpose_submatrix, transpose_transpose, add_comm]
simp_rw [transpose_apply]
