@[reducible, inline]

noncomputable abbrev HexPolyZMathlib.toPolyℚ (p : Hex.ZPoly) : Polynomial ℚ

The rational cast of an executable integer polynomial.

Equations

• HexPolyZMathlib.toPolyℚ p = Polynomial.map (Int.castRingHom ℚ) (HexPolyZMathlib.toPolynomial p)

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

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

theorem HexPolyZMathlib.toPolynomial_toRatPoly (f : Hex.ZPoly) : HexPolyMathlib.toPolynomial f.toRatPoly = toPolyℚ f

toRatPoly corresponds to the rational cast under toPolynomial.

@[simp]

theorem HexPolyZMathlib.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 HexPolyZMathlib.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 HexPolyZMathlib.toPolyℚ_ne_zero {f : Hex.ZPoly} (hf : f ≠ 0) : toPolyℚ f ≠ 0

The rational cast of a nonzero executable polynomial is nonzero.

theorem HexPolyZMathlib.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 HexPolyZMathlib.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.