The permutation expansion of the determinant (Four.I.3)

Open

hefferon_det_permutation_expansion

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

determinantlinear-algebrapermutations

For an $n \times n$ matrix $A$ over a commutative ring $K$ , the determinant is the sum, over all permutations $\sigma$ of $\{1,\dots,n\}$ , of the sign of $\sigma$ times the product $\prod_i A_{\sigma(i),i}$ .

Preamble

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

open Matrix

Formal statement

theorem hefferon_det_permutation_expansion
    {K : Type*} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :
    A.det = ∑ σ : Equiv.Perm (Fin n), Equiv.Perm.sign σ • ∏ i, A (σ i) i := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Four, Section I.3, Theorem 3.1, p. 349

View graph