theorem Hex.ZPoly.toRatPoly_derivative (f : ZPoly) : toRatPoly (DensePoly.derivative f) = f.toRatPoly.derivative

toRatPoly commutes with the formal derivative.

theorem Hex.ZPoly.modP_dvd_of_dvd {p : Nat} [ZMod64.Bounds p] {a b : ZPoly} (h : a ∣ b) : modP p a ∣ modP p b

Reduction modulo p preserves divisibility of integer polynomials.

def Hex.ZPoly.separableModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Bool

The 𝔽_p-separability certificate: the reduction of f and of its integer derivative are coprime over 𝔽_p.

Equations

• f.separableModP p = Hex.gcdIsUnit (Hex.DensePoly.gcd (Hex.ZPoly.modP p f) (Hex.ZPoly.modP p (Hex.DensePoly.derivative f)))

theorem Hex.ZPoly.squareFreeRat_of_separableModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hp : Nat.Prime p) (hadm : leadingCoeffAdmissible f p) (hsep : f.separableModP p = true) : f.SquareFreeRat

Modular square-freeness certificate soundness. For a prime p not dividing the leading coefficient of f, if modP f and modP f' are coprime over 𝔽_p, then f is square-free over ℚ.