23.1. Introduction🔗

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

HexBareiss is an executable fraction-free Bareiss determinant over a coefficient type with a caller-supplied exact quotient. Its retained integer entry point specializes that one implementation to a direct GMP-backed exact division call. On integer matrices every intermediate entry stays integral because each update divides exactly by the previous pivot. The algorithm runs in cubic time and 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 (and hence with Mathlib's Matrix.det), via the Desnanot-Jacobi invariant, is the last section.