hex

9.3. Constructors and normalization🔗

Every constructor routes through normalization so the no-trailing-zeros invariant holds by construction. Callers never trim by hand. The primitive normalizer drops trailing zeros from a raw array, and Hex.DensePoly.ofCoeffs wraps it to build a polynomial.

🔗def
Hex.DensePoly.trimTrailingZeros.{u} {R : Type u} [Zero R]
  [DecidableEq R] (coeffs : Array R) : Array R
Hex.DensePoly.trimTrailingZeros.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : Array R) : Array R

Normalize a coefficient array by discarding all trailing zeros. The compiled runtime uses the value-equal trimTrailingZerosImpl (proved by trimTrailingZeros_eq_impl, registered @[csimp]), which pops trailing zeros off the array in place instead of round-tripping through coeffs.toList.

🔗def
Hex.DensePoly.ofCoeffs.{u} {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : Array R) : Hex.DensePoly R
Hex.DensePoly.ofCoeffs.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (coeffs : Array R) : Hex.DensePoly R

Build a dense polynomial from a raw coefficient array by normalizing away trailing zeros.

🔗def
Hex.DensePoly.ofList.{u} {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : List R) : Hex.DensePoly R
Hex.DensePoly.ofList.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (coeffs : List R) : Hex.DensePoly R

Build a dense polynomial from a coefficient list by normalizing away trailing zeros.

The remaining constructors build the common shapes directly. The zero polynomial is the empty array; a constant collapses to zero when its scalar is zero; a monomial collapses likewise.

🔗def
Hex.DensePoly.zero.{u} {R : Type u} [Zero R] [DecidableEq R] :
  Hex.DensePoly R
Hex.DensePoly.zero.{u} {R : Type u}
  [Zero R] [DecidableEq R] :
  Hex.DensePoly R

The zero polynomial.

🔗def
Hex.DensePoly.C.{u} {R : Type u} [Zero R] [DecidableEq R] (c : R) :
  Hex.DensePoly R
Hex.DensePoly.C.{u} {R : Type u} [Zero R]
  [DecidableEq R] (c : R) :
  Hex.DensePoly R

Build the constant polynomial with value c. The zero constant collapses to the zero polynomial.

🔗def
Hex.DensePoly.monomial.{u} {R : Type u} [Zero R] [DecidableEq R] (n : ℕ)
  (c : R) : Hex.DensePoly R
Hex.DensePoly.monomial.{u} {R : Type u}
  [Zero R] [DecidableEq R] (n : ℕ)
  (c : R) : Hex.DensePoly R

Build the monomial c * x^n. The zero coefficient collapses to the zero polynomial.