2.6. Cross-references🔗

HexRowReduce depends only on HexMatrix, using its matrix type, arithmetic, and elementary operations.

• HexDeterminant and HexBareiss handle the determinant. Row reduction is the separate field-valued route for rank, span, and nullspace.

• HexRowReduceMathlib identifies the executable rank, span, and nullspace with their Mathlib analogues Matrix.rank, Submodule.span, and LinearMap.ker. HexRowReduce is Mathlib-free.