17.8. Cross-references🔗

HexGFq is the aggregator of the finite-field constructor libraries:

• HexConway supplies the committed Conway moduli and their Hex.Conway.SupportedEntry witnesses; each Hex.Conway.CommittedEntry instance wraps one.

• HexGFqField (over HexGFqRing) is the generic quotient field backing Hex.GFq and Hex.GFqC; every generic operation delegates to it.

• HexGF2 provides the single-word packed field GF2n backing Hex.GF2q, together with the GF2Poly.Irreducible predicate the packed certificates discharge.

HexGFq is Mathlib-free. Its Mathlib correspondence (above, via HexGFqMathlib) identifies the executable field with Mathlib's GaloisField.