10.1. Introduction🔗

HexPolyZ specializes HexPoly to integer coefficients and adds the integer-specific theory the factorization pipeline needs. It contributes three things: the content and primitive part (Gauss's-lemma factorization of an integer polynomial into a scalar times a primitive polynomial), a coefficientwise congruence predicate used by Hensel lifting, and a conservative executable Mignotte coefficient bound on the coefficients of any integer factor.

The library is Mathlib-free and depends only on HexPoly. HexHensel and the integer-factorization libraries consume it in turn. The mathematical justification of the Mignotte bound, that these executable quantities really do bound the coefficients of a factor, is proved in HexPolyZMathlib. See Cross-references.