Laplace's expansion along a row (Four.III.1)

Open

hefferon_laplace_expansion

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

cofactordeterminantlaplace-expansionlinear-algebra

Let $A$ be an $(n+1) \times (n+1)$ matrix over a commutative ring $K$ and fix a row index $i$ . Then $\det A = \sum_j (-1)^{i+j} A_{i,j} \det(A_{i,j}')$ , where $A_{i,j}'$ is the $n \times n$ minor obtained by deleting row $i$ and column $j$ .

Preamble

import Mathlib.Data.Matrix.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.ToLin

open Matrix

Formal statement

theorem hefferon_laplace_expansion
    {K : Type*} [CommRing K] {n : ℕ}
    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) K) (i : Fin (n + 1)) :
    A.det = ∑ j : Fin (n + 1),
      (-1) ^ ((i : ℕ) + (j : ℕ)) * A i j *
        (A.submatrix i.succAbove j.succAbove).det := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Four, Section III.1, Theorem 1.5, p. 376

View graph