3.6. Worked example🔗

The block below builds the integer matrix with rows (2, 0, 1), (1, 3, 2), and (0, 1, 1), whose determinant is 3. The identity has determinant one, the determinant is invariant under transpose, swapping two rows negates it, and a matrix with a dependent row pair is singular.

open Hex Hex.Matrix

namespace HexDeterminantChapterExample

-- A = [[2, 0, 1], [1, 3, 2], [0, 1, 1]], det = 3.
private def A : Matrix Int 3 3 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 2 | 0, 1 => 0 | 0, 2 => 1
    | 1, 0 => 1 | 1, 1 => 3 | 1, 2 => 2
    | 2, 0 => 0 | 2, 1 => 1 | 2, 2 => 1
    | _, _ => 0

-- The Leibniz determinant evaluates to 3.
#guard Matrix.det A = 3

-- The determinant is invariant under transpose.
#guard Matrix.det (Matrix.transpose A) = 3

-- Swapping two rows negates the determinant.
#guard Matrix.det (Matrix.rowSwap A 0 1) = -3

-- The identity has determinant one.
#guard Matrix.det (Matrix.identity (R := Int) 3) = 1

-- S = [[1, 2], [2, 4]] has a dependent row pair,
-- so its determinant is zero.
private def S : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 1 | 0, 1 => 2
    | 1, 0 => 2 | 1, 1 => 4
    | _, _ => 0

#guard Matrix.det S = 0

end HexDeterminantChapterExample