hex

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

Entrywise coefficient conversion commutes with the determinant through Hex.Matrix.det_mapEntries, given the four ring-homomorphism laws.