27.6. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexBareissTheory connects it to Mathlib. The final public umbrella exposes the correspondence over any commutative coefficient ring supplied with an exact quotient. The single law says that quotient cancels a known nonzero right factor; no public domain or nontriviality hypothesis is added.

theorem

HexMatrixTheory.bareissWith_eq_det.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (quot : R → R → R)
  (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a)
  (M : Hex.Matrix R n n) : Hex.Matrix.bareissWith quot M = M.det
HexMatrixTheory.bareissWith_eq_det.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (quot : R → R → R)
  (hquot :
    ∀ (a b : R),
      b ≠ 0 → quot (a * b) b = a)
  (M : Hex.Matrix R n n) :
  Hex.Matrix.bareissWith quot M = M.det

Row-pivoted Bareiss over an exact-division commutative ring agrees with Hex's executable determinant.

The matching theorem against Mathlib's determinant is available directly, without unfolding the generic loop or relying on definitional equality.

theorem

HexMatrixTheory.bareissWith_eq_mathlib_det.{u} {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ} (quot : R → R → R)
  (hquot : ∀ (a b : R), b ≠ 0 → quot (a * b) b = a)
  (M : Hex.Matrix R n n) :
  Hex.Matrix.bareissWith quot M = (HexMatrixTheory.matrixEquiv M).det
HexMatrixTheory.bareissWith_eq_mathlib_det.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] {n : ℕ}
  (quot : R → R → R)
  (hquot :
    ∀ (a b : R),
      b ≠ 0 → quot (a * b) b = a)
  (M : Hex.Matrix R n n) :
  Hex.Matrix.bareissWith quot M =
    (HexMatrixTheory.matrixEquiv M).det

Row-pivoted Bareiss over any commutative ring with an exact quotient agrees with Mathlib's determinant.

For integer matrices, Hex.Matrix.bareiss remains the specialization using the native exact-division primitive. Its original theorem names and premise-free statements remain the convenient compatibility surface.

theorem

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

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

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