Separability in terms of AdjoinRoot

A polynomial f over a commutative ring is separable, that is, coprime to its derivative, if and only if its derivative is a unit in R[X]/(f) (Polynomial.separable_iff_isUnit_mk_derivative). The right-hand side is the form in which separability enters standard étale presentations, where the derivative must be invertible modulo f.

This is kept apart from TauCeti.RingTheory.AdjoinRoot.Basic because Polynomial.Separable lives in Mathlib.FieldTheory.Separable, which the consumers of that file do not otherwise need.

theorem Polynomial.separable_iff_isUnit_mk_derivative {R : Type u_1} [CommRing R] {f : Polynomial R} : f.Separable ↔ IsUnit ((AdjoinRoot.mk f) (derivative f))

A polynomial is separable if and only if its derivative is a unit modulo it.