English
A determinant equals (-1)^{i0+j0} times the sum of column j0 entries times the determinant of the corresponding submatrix when all other columns sum to zero.
Русский
Детерминант равен (-1)^{i0+j0} умноженному на сумму элементов столбца j0 и детерминант соответствующей подматрицы, когда все остальные столбцы суммируются в ноль.
LaTeX
$$$\\det M = (-1)^{i_0+j_0} \\Bigl(\\sum_i M_{i j_0}\\Bigr) \\det\\bigl(M_{\\text{submatrix } (\\operatorname{succAbove} i_0) (\\operatorname{succAbove} j_0)}\\bigr)$$$
Lean4
/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row `i`. -/
theorem det_succ_row {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) :
det A = ∑ j : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove) :=
by
simp_rw [pow_add, mul_assoc, ← mul_sum]
have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by
calc
det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
_ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
rw [this, mul_assoc]
congr
rw [← det_permute, det_succ_row_zero]
refine Finset.sum_congr rfl fun j _ => ?_
rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]
congr 3
· rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_zero]
· ext i' j'
rw [Equiv.Perm.inv_def, Matrix.submatrix_apply, Matrix.submatrix_apply, Fin.cycleRange_symm_succ]
