5.5. Cross-references🔗

HexGramSchmidt depends only on HexMatrix and underpins HexLLL:

• HexMatrix supplies the Hex.Matrix representation and the row operations (rowAdd, rowSwap) that the update formulas reason about. The orthogonalization here is built entirely on that representation.

• HexGramSchmidtMathlib re-exports this executable theory as theorems about Mathlib's LinearMap and Matrix Gram-Schmidt. HexGramSchmidt itself imports only HexMatrix and Std.

• HexLLL consumes the integer data (the Gram determinants and scaled coefficients) and the exact update formulas to drive lattice reduction in integer arithmetic.