4.1. Introduction🔗

Released as hex-bareiss, with the Mathlib correspondence in hex-bareiss-mathlib.

HexBareiss is the executable fraction-free Bareiss determinant of a dense integer matrix: a Gaussian elimination in which every intermediate entry stays an exact integer because each update divides exactly by the previous pivot. It runs in cubic time and never leaves the integers, so it avoids both the factorial blow-up of the Leibniz determinant and the denominators of ordinary Gaussian elimination. It builds on HexMatrix and the HexDeterminant Leibniz determinant (the specification it is checked against).

HexBareiss is Mathlib-free. The theorem identifying the Bareiss determinant with the Leibniz determinant, via the Desnanot-Jacobi invariant, lives in HexBareissMathlib.