12.8. Cross-references🔗

Where HexGF2 fits in the executable DAG:

• HexPoly is the only dependency: it provides the generic dense-polynomial vocabulary against which the packed representation's arithmetic and Euclidean laws are stated. HexGF2 specializes that theory to the single-bit-coefficient case where the packed word layout and carry-less multiply apply.

• HexGF2 is consumed by the finite-field constructors that build on it (the packed characteristic-two entries of the GFq constructors), which reuse its GF2n/GF2nPoly wrappers and committed irreducibility certificates.

• HexGF2 is Mathlib-free. The Mathlib correspondence for the GF(2ⁿ) field theory is provided by the *Mathlib counterparts of the libraries that build on it, not by this library.