theorem HexRealRootsMathlib.isRoot_left_iff_of_mul_of_dvd_derivative {K : Type u_1} [Field K] [CharZero K] {q c r : Polynomial K} (hq : q ≠ 0) (hqcr : q = c * r) (hrd : r ∣ Polynomial.derivative q) (a : K) : c.IsRoot a ↔ q.IsRoot a

Field-generic square-free-core root transfer. Over a characteristic-zero field, if q = c * r (with q ≠ 0) and r divides the derivative q', then a point is a root of c iff it is a root of q. The root-multiplicity argument: at a root a of multiplicity m ≥ 1, q' has multiplicity m − 1 (characteristic zero), so r ∣ q' forces the r-multiplicity of a below m, leaving c with multiplicity at least one; conversely any root of c is a root of the product q. Hex-free; a candidate Mathlib contribution.

theorem HexRealRootsMathlib.aeval_eq_eval_toPolyℝ (q : Hex.ZPoly) (x : ℝ) : (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial q) = Polynomial.eval x (toPolyℝ q)

aeval at a real point of an embedded integer polynomial is the evaluation of its real cast.

theorem HexRealRootsMathlib.toPolyℝ_eq_map_toPolyℚ (q : Hex.ZPoly) : toPolyℝ q = Polynomial.map (algebraMap ℚ ℝ) (toPolyℚ q)

The real cast is the composition of the rational cast with ℚ → ℝ.

theorem HexRealRootsMathlib.toPolyℝ_repeatedPart_dvd_derivative (p : Hex.ZPoly) : toPolyℝ p.primitiveSquareFreeDecomposition.repeatedPart ∣ Polynomial.derivative (toPolyℝ p.primitivePart)

Executable-to-real divisibility. The real cast of the repeated part divides the derivative of the real cast of the primitive part: the executable rational divisibility, transported through ℚ and then ℚ → ℝ.

theorem HexRealRootsMathlib.aevalIff_squareFreeCore {p : Hex.ZPoly} (hp0 : p ≠ 0) (x : ℝ) : (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial p.squareFreeCore) = 0 ↔ (Polynomial.aeval x) (HexPolyZMathlib.toPolynomial p) = 0

Square-free core preserves real roots. A nonzero integer polynomial and its executable square-free core have exactly the same real roots, stated through aeval at real points. Shared with the rcf decision procedure (step 3) and consumed by the isolate_roots elaborator to reduce to square-free input.