English
Variant of row-sum determinant formula with submatrix removal and sign factor.
Русский
Вариант формулы детерминанта по строке с удалением подматрицы и знаком.
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 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 det_eq_sum_column_mul_submatrix_succAbove_succAbove_det {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R)
(i₀ j₀ : Fin (n + 1)) (hv : ∀ j ≠ j₀, ∑ i, M i j = 0) :
M.det = (-1) ^ (i₀ + j₀ : ℕ) * (∑ i, M i j₀) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det :=
by
rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]
simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]
rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]
conv_lhs =>
enter [2, 2, i]
rw [hv _ i.prop, mul_zero, zero_mul]
simp [Finset.sum_const_zero, add_zero]
