6.8. Cross-references🔗

• HexPoly supplies the dense representation behind the conversions and the Euclidean layer.

• HexBasic/ArrayDecEq.lean supplies the array equality instance the decidable equality routes through.

• HexSparsePolyMathlib is the proof boundary: it imports Mathlib, while HexSparsePoly and its executable consumers do not.