theorem HexPolyZTheory.size_le_one_iff_natDegree_eq_zero {R : Type u_1} [Semiring R] [DecidableEq R] (g : Hex.DensePoly R) : g.size ≤ 1 ↔ (HexPolyTheory.toPolynomial g).natDegree = 0

A dense polynomial stores at most one coefficient exactly when its Mathlib image has natural degree zero.

@[simp]

theorem HexPolyZTheory.coeff_toPolyℚ (p : Hex.ZPoly) (n : ℕ) : (toPolyℚ p).coeff n = ↑(Hex.DensePoly.coeff p n)

Coefficients of the rational cast are the rational casts of the integer coefficients.

theorem HexPolyZTheory.eval_toPolyℚ (p : Hex.ZPoly) (x : ℚ) : Polynomial.eval x (toPolyℚ p) = ∑ i ∈ Finset.range (Hex.DensePoly.size p), ↑(Hex.DensePoly.coeff p i) * x ^ i

Evaluation of the rational cast is the degree-indexed coefficient sum.

theorem HexPolyZTheory.toPolyℚ_ne_zero {f : Hex.ZPoly} (hf : f ≠ 0) : toPolyℚ f ≠ 0

The rational cast of a nonzero executable polynomial is nonzero.

theorem HexPolyZTheory.squareFreeRat_iff (f : Hex.ZPoly) (hf : f ≠ 0) : f.SquareFreeRat ↔ Squarefree (toPolyℚ f)

For a nonzero executable integer polynomial, the executable rational-gcd test is equivalent to squarefreeness of its rational cast.

theorem HexPolyZTheory.isRoot_squareFreeCore {f : Hex.ZPoly} (hf : f ≠ 0) {z : ℂ} (hz : (Polynomial.map (Int.castRingHom ℂ) (toPolynomial f)).IsRoot z) : (Polynomial.map (Int.castRingHom ℂ) (toPolynomial f.squareFreeCore)).IsRoot z

Passing to the executable square-free core preserves every complex root of a nonzero integer polynomial.