11.1. Introduction🔗

HexPolyFp specializes the executable dense polynomials to coefficients in Hex.ZMod64 p. Where HexPoly is generic over any coefficient type with a Zero and a DecidableEq, HexPolyFp fixes the coefficients to machine-word residues modulo a prime p and adds the operations that only make sense over `Fₚ`: modular exponentiation and composition in `Fₚ[x] / (f)`, the Frobenius-power maps X ↦ X^(pᵏ), square-free (Yun) decomposition, and the quotient by a modulus, which becomes a field exactly when the modulus is irreducible.

Hex.FpPoly is a thin abbrev over Hex.DensePoly, so the entire constructor, arithmetic, and Euclidean API documented in the HexPoly chapter is available unchanged. This chapter covers only what the prime-field specialization adds on top. HexPolyFp is Mathlib-free. It depends on HexPoly for the representation and on HexModArith for the ZMod64 p coefficient arithmetic. See Cross-references.