hex

14.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 : ℕ}
  (M : Hex.Matrix R n n) : R
Hex.Matrix.det.{u} {R : Type u}
  [Lean.Grind.Ring R] {n : ℕ}
  (M : Hex.Matrix R n n) : R

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

The classical row 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 : ℕ} : (Hex.Matrix.identity n).det = 1
Hex.Matrix.det_identity.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ} :
  (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 : ℕ}
  (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 : ℕ}
  (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 : ℕ}
  (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 : ℕ}
  (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 : ℕ}
  (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 : ℕ}
  (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 : ℕ} (M : Hex.Matrix R n n) : M.transpose.det = M.det
Hex.Matrix.det_transpose.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.Matrix R n n) :
  M.transpose.det = M.det

The determinant is invariant under matrix transpose.

Because the determinant is transpose-invariant, every row law has a column mirror, proved by transposing rather than by re-deriving anything: Hex.Matrix.det_colSwap, Hex.Matrix.det_colScale, and Hex.Matrix.det_colAdd correspond to the three row operations, and Hex.Matrix.det_setRow_add is the row mirror of the column linearity below.

🔗theorem
Hex.Matrix.det_colSwap.{u} {R : Type u} [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.Matrix R n n) (i j : Fin n) (h : i ≠ j) :
  (M.colSwap i j).det = -M.det
Hex.Matrix.det_colSwap.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : ℕ}
  (M : Hex.Matrix R n n) (i j : Fin n)
  (h : i ≠ j) :
  (M.colSwap i j).det = -M.det

Swapping two distinct columns negates the determinant. The column mirror of Hex.Matrix.det_rowSwap, proved by transposing to the row law.

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 : ℕ} (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 : ℕ}
  (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.