theorem Hex.DensePoly.eval_toPolynomial {R : Type u} [CommSemiring R] [DecidableEq R] (p : DensePoly R) (x : R) : p.eval x = Polynomial.eval x (HexPolyMathlib.toPolynomial p)

Horner evaluation of a dense polynomial agrees with evaluation after conversion to Mathlib's polynomial representation.

noncomputable def Hex.DensePoly.specialize {R : Type u} [CommRing R] [DecidableEq R] (f : DensePoly (DensePoly R)) (a : R) : Polynomial R

Specialize the coefficient variable of a dense bivariate polynomial while retaining its outer polynomial variable.

Equations

• f.specialize a = ∑ i ∈ Finset.range f.size, (Polynomial.monomial i) ((f.coeff i).eval a)

@[simp]

theorem Hex.DensePoly.coeff_specialize {R : Type u} [CommRing R] [DecidableEq R] (f : DensePoly (DensePoly R)) (a : R) (n : ℕ) : (f.specialize a).coeff n = (f.coeff n).eval a

Specialization evaluates each stored coefficient, with the dense zero extension supplying the coefficients outside the stored range.

@[simp]

theorem Hex.DensePoly.specialize_zero {R : Type u} [CommRing R] [DecidableEq R] (a : R) : specialize 0 a = 0

The zero dense polynomial specializes to the zero Mathlib polynomial.

noncomputable def Hex.DensePoly.evalBivariate {R : Type u} [CommRing R] [DecidableEq R] (f : DensePoly (DensePoly R)) (a b : R) : R

Evaluate a dense bivariate polynomial at (a, b).

Equations

• f.evalBivariate a b = Polynomial.eval b (f.specialize a)