8.7. Cross-references🔗

HexPolyFp builds on the generic dense polynomials and supplies the prime-field specialization the finite-field libraries use:

• HexPoly is the generic dense-polynomial library. Hex.FpPoly is an abbrev over Hex.DensePoly, so every constructor, arithmetic, evaluation, and Euclidean operation documented in that chapter is inherited at the specialized type. The concrete Hex.DensePoly.DivModLaws and Hex.DensePoly.GcdLaws the generic Euclidean laws are stated under are discharged here for Hex.ZMod64 at modulus p.

• HexModArith supplies Hex.ZMod64 at modulus p coefficient arithmetic: the machine-word modular add, multiply, and inverse that every operation in this chapter ultimately calls, along with the Hex.ZMod64.Bounds/Hex.ZMod64.PrimeModulus instances the prime-field operations require.

Downstream, the finite-field libraries consume HexPolyFp directly: HexGFqRing builds the quotient ring `Fₚ[x] / (g)` and HexGFqField promotes it to a field using the inverse laws documented above, each conditioned on irreducibility of the modulus, with the Hex.FpPoly.Irreducible witness produced by a checkable Rabin certificate from HexBerlekamp.

HexPolyFp is Mathlib-free. Its Mathlib correspondence is HexPolyFpMathlib, documented in The Mathlib correspondence above, which identifies Hex.FpPoly with Polynomial (ZMod p) and carries the CommRing instance that every ring homomorphism out of the executable polynomials needs. Nothing in this chapter depends on it: the modular exponentiation, the Frobenius maps, the square-free decomposition, and the quotient are all executable and Mathlib-free.