19.7. Mathematical algorithms🔗

The tactics are only the proof-producing user interface. The underlying algorithms are described separately:

• finite-field Berlekamp factorization explains Frobenius fixed spaces and Rabin certificates;

• integer Berlekamp-Zassenhaus factorization explains normalization, Hensel lifting, subset recombination, and logarithmic-derivative lattice recombination;

• HexHensel gives the lifting constructions;

• HexLLL gives the certified lattice reduction used during lattice recombination.