9.1. Introduction🔗

HexPoly stores an executable dense polynomial as an Array of coefficients in ascending degree order: index i holds the coefficient of xⁱ. The array carries a single structural invariant: no trailing zeros. This normalized representation makes structural equality coincide with semantic equality, so two HexPoly polynomials are equal as Lean values exactly when they are equal as polynomials.

Hex.DensePoly is generic over any coefficient type R with a Zero and a DecidableEq. The arithmetic, evaluation, and Euclidean operations require the further structure (Add, Mul, Sub, Div) that each one needs. HexPoly is Mathlib-free and depends on no other hex library. The integer library HexPolyZ, the prime-field library HexPolyFp, and through them the factorization and finite-field libraries all consume this representation. See Cross-references.