14.8. 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 Hex.Matrix.det as its Leibniz specification.

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