3.7. Cross-references🔗

HexDeterminant depends only on HexMatrix, using its matrix type, arithmetic, and elementary operations (whose determinant laws are proved here).

• HexBareiss computes the same integer determinant fraction-free in cubic time, using this Leibniz det as its specification.

• HexDeterminantMathlib identifies this executable determinant with Mathlib's Matrix.det. HexDeterminant itself is Mathlib-free.