14.5. Cross-references🔗

HexGFqRing depends on a polynomial-arithmetic library, and a finite-field library depends on it:

HexPolyFp provides the Hex.FpPoly representation that Hex.GFqRing.reduceMod operates on, together with the Hex.DensePoly.divMod and Hex.DensePoly.mod operations from which reduceMod is built. The univariate polynomial division laws packaged there are what justify the canonical-representative invariant.
HexGFqField specializes the same quotient to an irreducible modulus and adds the field structure. The FiniteField type in HexGFqField is a thin wrapper carrying a Hex.GFqRing.PolyQuotient value plus the irreducibility hypothesis, so every operation in HexGFqField reduces through the same reduceMod and the same canonical-representative invariant documented in this chapter. Downstream callers such as HexConway reach HexGFqRing transitively through HexGFqField.

14.5.1. No Mathlib correspondence library🔗

Some hex-* libraries pair the executable library with a *Mathlib correspondence library that re-exports the executable API as theorems about the corresponding Mathlib structures. HexGFqRing has no such correspondence library: there is no HexGFqRingMathlib, and the chapter therefore does not contain the "computational vs. Mathlib correspondence" cross-reference that future chapters will include for libraries that have one.

For HexGFqRing the canonical mathematical home of the quotient is Mathlib's AdjoinRoot or Polynomial.quotient construction. A correspondence between Hex.GFqRing.PolyQuotient and those constructions is deferred to a downstream library if and when a Mathlib-valued caller needs it.