6.8. Cross-references🔗

HexPolyZ builds on the base polynomial representation and feeds the integer-factorization libraries:

• HexPoly is the generic dense-polynomial library this one specializes. The constructors, arithmetic, and Euclidean operations used throughout this chapter (the #p[...] literal, Hex.DensePoly.scale, and the rational division underlying Hex.ZPoly.primitiveSquareFreeDecomposition) are documented there. HexPolyZ only fixes the coefficient type to Int and adds the content, congruence, and Mignotte operations.

• HexPolyZMathlib is the correspondence library: it identifies Hex.ZPoly with Mathlib's Polynomial ℤ and proves the Mignotte bound as a theorem about the Mahler measure of the corresponding Polynomial ℤ. The executable quantities in this chapter compute the bound that theorem proves valid. The Mathlib dependency lives entirely there, never inside HexPolyZ itself.

• HexHensel consumes the congruence predicate and Hex.ZPoly.defaultFactorCoeffBound to drive the Hensel-lifting and coefficient-recovery steps of integer polynomial factorization.