theorem Hex.AlgebraicPoly.toPolynomial_ofArray (coeffs : Array AlgebraicNumber) : (ofArray coeffs).toPolynomial = Array.foldr (fun (a : AlgebraicNumber) (p : Polynomial ℂ) => Polynomial.C a.toComplex + Polynomial.X * p) 0 coeffs

Removing trailing canonical zero coefficients preserves the polynomial.

theorem Hex.AlgebraicPoly.coeff_ofArray (coeffs : Array AlgebraicNumber) (n : ℕ) : (ofArray coeffs).toPolynomial.coeff n = (coeffs.getD n 0).toComplex

Normalization preserves every coefficient, including implicit trailing zeros.

noncomputable def Hex.AlgebraicPoly.ofPolynomial (p : Polynomial AlgebraicNumber) : AlgebraicPoly

Represent a Mathlib polynomial by its finite coefficient array.

Equations

• Hex.AlgebraicPoly.ofPolynomial p = Hex.AlgebraicPoly.ofArray (Array.ofFn fun (i : Fin (p.natDegree + 1)) => p.coeff ↑i)

theorem Hex.AlgebraicPoly.toPolynomial_ofPolynomial (p : Polynomial AlgebraicNumber) : (ofPolynomial p).toPolynomial = Polynomial.map AlgebraicNumber.toComplexHom p

Conversion preserves the complex interpretation of the polynomial.