14.7. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexDeterminantMathlib connects it to Mathlib: the Leibniz determinant Hex.Matrix.det equals Mathlib's Matrix.det of the corresponding Mathlib matrix, transported through HexMatrixMathlib.matrixEquiv (the same equivalence the HexMatrix chapter introduces).

theorem

HexMatrixMathlib.det_eq.{u} {R : Type u} {n : ℕ} [CommRing R]
  (M : Hex.Matrix R n n) : M.det = (HexMatrixMathlib.matrixEquiv M).det
HexMatrixMathlib.det_eq.{u} {R : Type u}
  {n : ℕ} [CommRing R]
  (M : Hex.Matrix R n n) :
  M.det =
    (HexMatrixMathlib.matrixEquiv M).det

The executable Leibniz determinant Hex.Matrix.det agrees with Mathlib's Matrix.det of the corresponding matrix under HexMatrixMathlib.matrixEquiv. This bridge lets a fact about Matrix.det be discharged by running the executable determinant, or lets the executable determinant be analyzed with Mathlib's determinant theory.

So a fact about Mathlib's Matrix.det can be discharged by running the executable determinant, and a fact about the executable determinant can be proved with Mathlib's determinant theory.