9.2. Dense polynomial type🔗

The normalization invariant is a predicate on coefficient arrays, and the polynomial type is the array bundled with a proof of that predicate.

def

Hex.DensePolyNormalized.{u} {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : Array R) : Prop
Hex.DensePolyNormalized.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (coeffs : Array R) : Prop

DensePolyNormalized coeffs means either coeffs is empty or its last coefficient is nonzero, so the array has no trailing zeros.

structure

Hex.DensePoly.{u} (R : Type u) [Zero R] [DecidableEq R] : Type u
Hex.DensePoly.{u} (R : Type u) [Zero R]
  [DecidableEq R] : Type u

Dense polynomials store coefficients in ascending degree order, with index i holding the coefficient of x^i.

Constructor

Hex.DensePoly.mk.{u}

Fields

coeffs : Array R

The stored coefficients in ascending degree order.

normalized : Hex.DensePolyNormalized self.coeffs

Proof that coeffs carries no trailing zeros.

Because the invariant pins down a unique array for each polynomial value, HexPoly derives a DecidableEq on Hex.DensePoly and proves the extensionality principle: two normalized polynomials are equal as soon as their coefficient functions agree.

theorem

Hex.DensePoly.ext_coeff.{u} {R : Type u} [Zero R] [DecidableEq R]
  {p q : Hex.DensePoly R} (hcoeff : ∀ (i : ℕ), p.coeff i = q.coeff i) :
  p = q
Hex.DensePoly.ext_coeff.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  {p q : Hex.DensePoly R}
  (hcoeff :
    ∀ (i : ℕ), p.coeff i = q.coeff i) :
  p = q

Extensionality for normalized dense polynomials by their coefficient functions. This is the preferred form of extensionality: it asks only for coefficient agreement, since size agreement is forced (via size_eq_of_coeff_eq).