hex

11.2. The prime-field polynomial type🔗

A prime-field polynomial is a dense polynomial whose coefficients are ZMod64 p residues. The ZMod64.Bounds p instance carries the proof that p fits in a machine word, so arithmetic stays in the fast path.

🔗def
Hex.FpPoly (p : Nat) [Hex.ZMod64.Bounds p] : Type
Hex.FpPoly (p : Nat)
  [Hex.ZMod64.Bounds p] : Type

Executable dense polynomials over the prime-field candidate ZMod64 p.

Because Hex.FpPoly unfolds to Hex.DensePoly, the HexPolyFp namespace re-exports the constructors and queries a caller needs for the specialized type. Hex.FpPoly.ofCoeffs builds a polynomial from a coefficient array, Hex.FpPoly.X is the indeterminate, and Hex.FpPoly.modByMonic reduces modulo a monic divisor. The irreducibility predicate the field operations require as a hypothesis is also stated here.

🔗def
Hex.FpPoly.Irreducible {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Prop
Hex.FpPoly.Irreducible {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Prop

Polynomial irreducibility over F_p phrased as the absence of nontrivial factorizations inside the executable dense-polynomial model.