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 unconditionally (with no side hypothesis) and is the preferred surface for downstream Mathlib-side callers.