3.2. The Leibniz determinant🔗

The reference determinant is the Leibniz formula: a signed sum over all permutations of the product of the selected entries.

def

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

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

The classical row and column laws are all proved against this definition. The identity has determinant one; swapping two rows negates the determinant; scaling a row scales it; adding a multiple of one row to another leaves it unchanged; and the determinant is invariant under transpose.

theorem

Hex.Matrix.det_identity.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} : (Hex.Matrix.identity n).det = 1
Hex.Matrix.det_identity.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat} :
  (Hex.Matrix.identity n).det = 1

The determinant of the identity matrix is one.

theorem

Hex.Matrix.det_rowSwap.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n) (i j : Fin n) (h : i ≠ j) :
  (M.rowSwap i j).det = -M.det
Hex.Matrix.det_rowSwap.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (i j : Fin n)
  (h : i ≠ j) :
  (M.rowSwap i j).det = -M.det

Swapping two distinct rows negates the determinant.

theorem

Hex.Matrix.det_rowScale.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n) (i : Fin n) (c : R) :
  (M.rowScale i c).det = c * M.det
Hex.Matrix.det_rowScale.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (i : Fin n)
  (c : R) :
  (M.rowScale i c).det = c * M.det

Scaling a row by c scales the determinant by c.

theorem

Hex.Matrix.det_rowAdd.{u} {R : Type u} [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (src dst : Fin n) (c : R) (h : src ≠ dst) :
  (M.rowAdd src dst c).det = M.det
Hex.Matrix.det_rowAdd.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (src dst : Fin n)
  (c : R) (h : src ≠ dst) :
  (M.rowAdd src dst c).det = M.det

Adding a multiple of one row to a distinct row preserves the determinant.

theorem

Hex.Matrix.det_transpose.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n) : M.transpose.det = M.det
Hex.Matrix.det_transpose.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) :
  M.transpose.det = M.det

The determinant is invariant under matrix transpose.

theorem

Hex.Matrix.det_colSwap.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n) (i j : Fin n) (h : i ≠ j) :
  (Hex.Matrix.ofFn fun r c => M[r][Hex.Matrix.finTranspose i j c]).det =
    -M.det
Hex.Matrix.det_colSwap.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (i j : Fin n)
  (h : i ≠ j) :
  (Hex.Matrix.ofFn fun r c =>
        M[r][Hex.Matrix.finTranspose i j
            c]).det =
    -M.det

Swapping two columns negates determinant.

The determinant is linear in each column separately. The additive law in one column is the building block for Laplace expansion.

theorem

Hex.Matrix.det_setCol_add.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R n n) (dst : Fin n) (v w : Fin n → R) :
  (M.setCol dst fun r => v r + w r).det =
    (M.setCol dst v).det + (M.setCol dst w).det
Hex.Matrix.det_setCol_add.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R n n) (dst : Fin n)
  (v w : Fin n → R) :
  (M.setCol dst fun r => v r + w r).det =
    (M.setCol dst v).det +
      (M.setCol dst w).det

Determinant linearity in one replaced column, additive form.