10.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 (ofCoeffs, scale, the rational division underlying 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 the defaultFactorCoeffBound to drive the Hensel-lifting and coefficient-recovery steps of integer polynomial factorization.