3.1. Introduction🔗

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

HexDeterminant is the determinant of a dense square matrix via the Leibniz formula, with the cofactor and adjugate theory built on it. It depends only on HexMatrix and is generic over the coefficient ring. The row-operation, Laplace, Cauchy-Binet, and Plücker results hold over a commutative ring.

The Leibniz determinant is the definition: correct by construction but factorially slow, so it is the specification the faster HexBareiss route is checked against, not the routine a caller runs on a large matrix.

HexDeterminant is Mathlib-free. The identification of this determinant with Mathlib's Matrix.det, and with the executable Bareiss determinant, lives in HexDeterminantMathlib and HexBareissMathlib.