hex

2.3. Constructors and normalization🔗

Every constructor uses 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 in-place implementation below, registered through @[csimp], which pops trailing zeros off the array 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.

For a coefficient literal, #p[a₀, a₁, ...] constructs the same value as Hex.DensePoly.ofCoeffs applied to #[a₀, a₁, ...]. The expected dense-polynomial type determines the coefficient type. Coefficients are listed in ascending degree order, so aᵢ is the coefficient of xⁱ. The literal uses the same normalization as ofCoeffs, including removal of 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.