det_succ_row_zero — Mathlib

English

Determinant expansion along a fixed row i expresses det as a sum of cofactors along that row.

Русский

Разложение детерминанта по произвольной строке i выражает det как сумму кофакторов по этой строке.

LaTeX

$$$\\det A = \\sum_{j=0}^{n} (-1)^{i+j} A_{ij} \\det\\bigl(A_{\\text{submatrix } (i) (j)}\\bigr)$$$

Lean4

/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row 0. -/
theorem det_succ_row_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :
    det A = ∑ j : Fin n.succ, (-1) ^ (j : ℕ) * A 0 j * det (A.submatrix Fin.succ j.succAbove) :=
  by
  rw [← det_transpose A, det_succ_column_zero]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [← det_transpose]
  simp only [transpose_apply, transpose_submatrix, transpose_transpose]

Похожие утверждения