Squarefree polynomials over a perfect field

A candidate for Mathlib.FieldTheory.Perfect: a squarefree polynomial over a perfect field and its derivative have no common root (Squarefree.eval_ne_zero_or_eval_derivative_ne_zero), since it is separable.

theorem Squarefree.eval_ne_zero_or_eval_derivative_ne_zero {K : Type u_1} [Field K] [PerfectField K] {p : Polynomial K} (hp : Squarefree p) (x : K) : Polynomial.eval x p ≠ 0 ∨ Polynomial.eval x (Polynomial.derivative p) ≠ 0

A squarefree polynomial over a perfect field and its derivative have no common root.