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 polynomialf
is separable iff it is coprime with its derivative.
A polynomial is separable iff it is coprime with its derivative.
Instances For
A separable polynomial is square-free.
See PerfectField.separable_iff_squarefree
for the converse when the coefficients are a perfect
field.
If a non-zero polynomial splits, then it has no repeated roots on that field if and only if it is separable.
If a non-zero polynomial over F
splits in K
, then it has no repeated roots on K
if and only if it is separable.
Typeclass for separable field extension: K
is a separable field extension of F
iff
the minimal polynomial of every x : K
is separable. This implies that K/F
is an algebraic
extension, because the minimal polynomial of a non-integral element is 0
, which is not
separable.
We define this for general (commutative) rings and only assume F
and K
are fields if this
is needed for a proof.
- separable' : ∀ (x : K), (minpoly F x).Separable
Instances
If the minimal polynomial of x : K
over F
is separable, then x
is integral over F
,
because the minimal polynomial of a non-integral element is 0
, which is not separable.
Transfer IsSeparable
across an AlgEquiv
.
Equations
- ⋯ = ⋯
A finite field extension in characteristic 0 is separable.
Equations
- ⋯ = ⋯
If R / K / A
is an extension tower, x : R
is separable over A
, then it's also separable
over K
.