theorem HexRootsMathlib.hasOnlySimpleRoots_iff_squarefree (p : Hex.ZPoly) (hp : p ≠ 0) : Hex.HasOnlySimpleRoots p ↔ Squarefree (HexPolyZMathlib.toPolyℚ p)

On nonzero inputs, the executable simple-root predicate is exactly squarefreeness of the rational cast.

theorem HexRootsMathlib.hasOnlySimpleRoots_iff_separable (p : Hex.ZPoly) (hp : p ≠ 0) : Hex.HasOnlySimpleRoots p ↔ (HexPolyZMathlib.toPolyℚ p).Separable

Equivalent separability form of the executable simple-root predicate.

theorem HexRootsMathlib.HasOnlySimpleRoots.separable {p : Hex.ZPoly} (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) : (HexPolyZMathlib.toPolyℚ p).Separable

A nonzero executable polynomial with only simple roots has separable rational cast.