15.5. 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 Bareiss route agrees with the Leibniz determinant on it, the identity has determinant one, and a matrix with a dependent row pair is singular.

open Hex Hex.Matrix

namespace HexBareissChapterExample

-- 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 Bareiss determinant is 3, agreeing with Leibniz.
#guard bareiss A = 3
#guard bareiss A = det A

-- The packaged record reads off the same determinant.
#guard (bareissData A).det = 3

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

-- S = [[1, 2], [2, 4]]: dependent rows, so singular.
private def S : Hex.Matrix Int 2 2 := #m[1, 2; 2, 4]

#guard bareiss S = 0

end HexBareissChapterExample