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)

theorem Hex.Matrix.det_mapEntries {S : Type v} {R : Type u} [Lean.Grind.CommRing R] [Lean.Grind.CommRing S] {n : Nat} (M : Matrix R n n) (f : R → S) (hzero : f 0 = 0) (hone : f 1 = 1) (hadd : ∀ (a b : R), f (a + b) = f a + f b) (hmul : ∀ (a b : R), f (a * b) = f a * f b) : (M.mapEntries f).det = f M.det

The Leibniz determinant commutes with an entrywise ring homomorphism. The homomorphism laws are explicit to keep this statement Mathlib-free.

@[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.