19.1. Introduction🔗

factor_poly produces a certified factorization of a concrete polynomial. irreducibility proves that a concrete polynomial is irreducible. Both commands run compiled search during elaboration and emit a proof term containing only reified data and verified certificate checks.

The supported input types depend on the imported library:

• HexBerlekamp supports Hex.FpPoly;

• HexBerlekampMathlib adds Polynomial (ZMod p);

• HexBerlekampZassenhaus adds Hex.ZPoly;

• HexBerlekampZassenhausMathlib adds Polynomial ℤ.