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.IsSeparable K x
: an elementx
is separable overK
iff the minimal polynomial ofx
overK
is separable.Algebra.IsSeparable K L
:L
is separable overK
iff every element inL
is separable overK
.
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.
An element x
of an algebra K
over a commutative ring F
is said to be separable, if its
minimal polynomial over K
is separable. Note that the minimal polynomial of any element not
integral over F
is defined to be 0
, which is not a separable polynomial.
Equations
- IsSeparable F x = (minpoly F x).Separable
Instances For
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.
- isSeparable' : ∀ (x : K), IsSeparable F x
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.
Equations
- ⋯ = ⋯
Transfer IsSeparable
across an AlgEquiv
.
Transfer Algebra.IsSeparable
across an AlgEquiv
.
Alias of AlgEquiv.Algebra.isSeparable
.
Transfer Algebra.IsSeparable
across an AlgEquiv
.
If E / L / F
is a scalar tower and x : E
is separable over F
, then it's also separable
over L
.
Equations
- ⋯ = ⋯
A integral field extension in characteristic 0 is separable.
Equations
- ⋯ = ⋯
If E / K / F
is a scalar tower and algebraMap K E x
is separable over F
, then x
is
``
also separable over F
.