22.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.

The same public umbrella re-exports the bordered-minor form of Desnanot--Jacobi used by fraction-free elimination. It is stated over an arbitrary commutative ring and remains separate from the executable layer.

theorem

HexMatrixMathlib.desnanot_jacobi_borderedMinor.{u} {R : Type u} {n : ℕ}
  [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hk : k < n)
  (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) :
  (source.borderedMinor (k + 1) hnext i j).det *
      (source.principalSubmatrix k ⋯).det =
    (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det *
        (source.borderedMinor k hk i j).det -
      (source.borderedMinor k hk i ⟨k, ⋯⟩).det *
        (source.borderedMinor k hk ⟨k, ⋯⟩ j).det
HexMatrixMathlib.desnanot_jacobi_borderedMinor.{u}
  {R : Type u} {n : ℕ} [CommRing R]
  (source : Hex.Matrix R n n) (k : ℕ)
  (hk : k < n) (hnext : k + 1 < n)
  (i j : Fin n) (hi : k < ↑i)
  (hj : k < ↑j) :
  (source.borderedMinor (k + 1) hnext i
          j).det *
      (source.principalSubmatrix k
          ⋯).det =
    (source.borderedMinor k hk ⟨k, ⋯⟩
            ⟨k, ⋯⟩).det *
        (source.borderedMinor k hk i
            j).det -
      (source.borderedMinor k hk i
            ⟨k, ⋯⟩).det *
        (source.borderedMinor k hk ⟨k, ⋯⟩
            j).det

Desnanot-Jacobi specialised to a Bareiss bordered minor: the Mathlib determinant identity from desnanot_jacobi_borderedMinor_reindex translated back into Hex borderedMinor/principalSubmatrix determinants. This produces the hdesnanot premise expected by bareissExactDiv_borderedMinor_of_mul_eq with prevPivot instantiated as det (principalSubmatrix source k _).