Separable polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We define a polynomial to be separable if it is coprime with its derivative. We prove basic
properties about separable polynomials here.
Main definitions #
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.