3.7. Cross-references🔗

• HexPoly supplies the dense polynomial used by the recursive view.

• HexBasic/ExtTreeMap.lean contains the reusable ordered-map algorithms used by sparse addition and canonicalization.

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