def Hex.ZPoly.ratSquarefree (p : DensePoly Rat) : Bool

Exact squarefreeness over the rational base field, excluding zero.

Equations

• Hex.ZPoly.ratSquarefree p = (!p.isZero && decide ((p.gcd p.derivative).size ≤ 1))

def Hex.ZPoly.ratSquarefreeFast (p : DensePoly Rat) : Bool

Try the verified modular certificate on the integer primitive part before running the exact rational gcd. Bad reduction is inconclusive and retains the exact fallback, including primes dividing the leading coefficient.

Equations

• Hex.ZPoly.ratSquarefreeFast p = (!p.isZero && (Hex.modularSquareFreeCoreFires (Hex.ZPoly.ratPolyPrimitivePart p) || decide ((p.gcd p.derivative).size ≤ 1)))

@[csimp]

theorem Hex.ZPoly.ratSquarefree_eq_fast : ratSquarefree = ratSquarefreeFast

The modular trial changes only the compiled computation, preserving the exact gcd-based predicate used by the correspondence proofs.