hex

15.5. Cross-references🔗

HexGFqField has two upstream dependencies and serves the finite-field-valued callers downstream:

  • HexGFqRing (see its chapter) supplies the underlying Hex.GFqRing.PolyQuotient representation and all of the ring arithmetic. A FiniteField is a one-field wrapper around a PolyQuotient, and every field operation reduces through the same Hex.GFqRing.reduceMod, so the canonical-representative invariant documented there carries over verbatim.

  • HexBerlekamp provides the irreducibility infrastructure. The Hex.FpPoly.Irreducible hypothesis carried by every field element is, in practice, produced from a checkable Rabin Hex.Berlekamp.IrreducibilityCertificate via Hex.Berlekamp.rabinTest_imp_irreducible, as shown in the worked example above.

Downstream, HexConway builds Conway polynomials and canonical GF(pⁿ) constructions on top of this field, reaching HexGFqRing transitively through HexGFqField.

15.5.1. No Mathlib correspondence library🔗

Like HexGFqRing, HexGFqField is a purely computational library with no paired *Mathlib correspondence: there is no HexGFqFieldMathlib, and this chapter therefore carries no "computational vs. Mathlib correspondence" cross-reference. The canonical mathematical home of GF(pⁿ) is Mathlib's GaloisField / AdjoinRoot construction. A correspondence between Hex.GFqField.FiniteField and those structures is deferred to a downstream library if and when a Mathlib-valued caller needs it.