Theory of univariate polynomials #
This file starts looking like the ring theory of $ R[X] $
f is a polynomial over a field, and
a : K satisfies
f' a ≠ 0,
f / (X - a) is coprime with
X - a.
Note that we do not assume
f a = 0, because
f / (X - a) = (f - f a) / (X - a).