Core Leibniz-formula definitions for the dense determinant.

This module defines the determinant det of a dense square matrix as the permutationVectors-indexed sum of signed Leibniz terms, built from detSign (the inversion-parity sign of a permutation vector), detProduct (the unsigned diagonal product), and detTerm (their product). It records the small base cases det_one_by_one, det_two_by_two, and det_principalSubmatrix_zero, and provides the reusable foldl-arithmetic toolkit (scalar factoring, additive splitting, permutation invariance, single-index scaling) plus the Fin.castSucc/Fin.last inversion-count lemmas used by the recursive determinant proofs in the sibling modules.

def Hex.Matrix.detSign {R : Type u} [Lean.Grind.Ring R] {n : Nat} (perm : Vector (Fin n) n) : R

The sign of a permutation vector, computed from inversion parity.

Equations

• Hex.Matrix.detSign perm = if Hex.Matrix.inversionCount perm.toList % 2 = 0 then 1 else -1

def Hex.Matrix.detProduct {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R n n) (perm : Vector (Fin n) n) : R

The unsigned product associated to a permutation vector.

Equations

• M.detProduct perm = Fin.foldl n (fun (acc : R) (i : Fin n) => acc * M[(i, perm[i])]) 1

def Hex.Matrix.detTerm {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R n n) (perm : Vector (Fin n) n) : R

The Leibniz summand associated to a permutation vector.

Equations

• M.detTerm perm = Hex.Matrix.detSign perm * M.detProduct perm

def Hex.Matrix.det {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R n n) : R

The determinant of a dense square matrix, defined by the Leibniz formula.

Equations

• M.det = List.foldl (fun (acc : R) (perm : Vector (Fin n) n) => acc + M.detTerm perm) 0 (Hex.Matrix.permutationVectors n)

@[simp]

theorem Hex.Matrix.det_principalSubmatrix_zero {n : Nat} {R : Type u} [Lean.Grind.Ring R] (M : Matrix R n n) : (M.principalSubmatrix 0 ⋯).det = 1

The determinant of the empty leading prefix is the Bareiss previous-pivot convention 1.

@[simp]

theorem Hex.Matrix.det_one_by_one {R : Type u} [Lean.Grind.Ring R] (M : Matrix R 1 1) : M.det = M[0][0]

The determinant of a 1 × 1 matrix is its only entry. This is the smallest non-empty determinant base case.

@[simp]

theorem Hex.Matrix.det_two_by_two {R : Type u} [Lean.Grind.CommRing R] (M : Matrix R 2 2) : M.det = M[0][0] * M[1][1] - M[1][0] * M[0][1]

The determinant of a 2 × 2 matrix has the usual diagonal-minus-off-diagonal closed form used by small cofactor expansions.