14.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 : Hex.Matrix Int 3 3 :=
  #m[2, 0, 1; 1, 3, 2; 0, 1, 1]

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

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

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

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

-- S = [[1, 2], [2, 4]] has a dependent row pair,
-- so its determinant is zero.
private def S : Hex.Matrix Int 2 2 := #m[1, 2; 2, 4]

#guard det S = 0

end HexDeterminantChapterExample