noncomputable def Hex.AlgebraicPoly.toPolynomial (f : AlgebraicPoly) : Polynomial ℂ

Interpret a normalized executable algebraic polynomial in Polynomial ℂ.

Equations

• f.toPolynomial = Array.foldr (fun (a : Hex.AlgebraicNumber) (value : Polynomial ℂ) => Polynomial.C a.toComplex + Polynomial.X * value) 0 f.coeffs

theorem Hex.AlgebraicPoly.coeff_toPolynomial (f : AlgebraicPoly) (n : ℕ) : f.toPolynomial.coeff n = (f.coeff n).toComplex

Semantic coefficients agree with the executable coefficient accessor.

theorem Hex.AlgebraicPoly.last_isZero_false (f : AlgebraicPoly) (h : (!f.isZero) = true) : (f.coeff (f.size - 1)).isZero = false

The stored leading coefficient of a nonzero normalized algebraic polynomial is canonically nonzero.

theorem Hex.AlgebraicPoly.isZero_iff (f : AlgebraicPoly) : f.isZero = true ↔ f.toPolynomial = 0

Executable semantic-zero detection is exact.

theorem Hex.AlgebraicPoly.natDegree_toPolynomial (f : AlgebraicPoly) (h : (!f.isZero) = true) : f.toPolynomial.natDegree = f.natDegree

A nonzero executable polynomial has the same natural degree as its semantic interpretation.

theorem Hex.AlgebraicPoly.beq_iff (f g : AlgebraicPoly) : (f == g) = true ↔ f.toPolynomial = g.toPolynomial

Canonical coefficientwise Boolean equality is faithful to the semantic polynomial interpretation.