18.9. Relationship to the tactics🔗

The factor_poly and irreducibility tactics described in the factor-tactics chapter use this factorization code as certificate search. Their emitted proof terms contain reified polynomial data and verified certificate checks, not an invocation of the factorization algorithm.