Separable polynomials #
We define a polynomial to be separable if it is coprime with its derivative. We prove basic
properties about separable polynomials here.
Main definitions #
polynomial.separable f: a polynomial
f is separable iff it is coprime with its derivative.
polynomial.expand R p f: expand the polynomial
f with coefficients in a
R by a factor of p, so
expand R p (∑ aₙ xⁿ) is
∑ aₙ xⁿᵖ.
polynomial.contract p f: the opposite of
expand, so it sends
∑ aₙ xⁿᵖ to
∑ aₙ xⁿ.
A polynomial is separable iff it is coprime with its derivative.
n ≠ 0 in
X ^ n - a is separable for any
a ≠ 0.
In a field
X ^ n - 1 is separable iff
↑n ≠ 0.
Typeclass for separable field extension:
K is a separable field extension of
the minimal polynomial of every
x : K is separable.
We define this for general (commutative) rings and only assume
K are fields if this
is needed for a proof.
Instances of this typeclass
A finite field extension in characteristic 0 is separable.