hex

15.6. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexBareissMathlib connects it to Mathlib. Its headline theorem is that the fraction-free Bareiss determinant equals the Leibniz determinant on integer square matrices, so the cubic-time route and the specification agree outright.

🔗theorem
HexMatrixMathlib.bareiss_eq_det {n : ℕ} (M : Hex.Matrix ℤ n n) :
  M.bareiss = M.det
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.

Composed with the determinant correspondence, this also identifies the Bareiss determinant with Mathlib's Matrix.det.

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

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