The HexBareissMathlib library is the Mathlib bridge for hex-bareiss. It exposes the row-pivoted Bareiss determinant correctness theorems against both Mathlib's determinant and the executable Leibniz determinant, building on the no-pivot bordered-minor invariant in HexBareissMathlib.Bareiss and the determinant correspondence in HexDeterminantMathlib.

theorem HexMatrixMathlib.bareissDet_eq_det {n : ℕ} (M : Hex.Matrix ℤ n n) : M.bareiss = (matrixEquiv M).det

Row-pivoted Bareiss determinant soundness, exposed against Mathlib's determinant for downstream Mathlib-side callers.

theorem HexMatrixMathlib.bareiss_eq_det {n : ℕ} (M : Hex.Matrix ℤ n n) : M.bareiss = M.det

The row-pivoted Bareiss determinant equals the executable Leibniz determinant on integer square matrices. Proven Mathlib-side by composing bareiss_eq_mathlib_det with det_eq, so it holds outright (no sorry-bound hypothesis) and is the preferred surface for downstream Mathlib-side callers.