Split polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A polynomial f : K[X]
splits over a field extension L
of K
if it is zero or all of its
irreducible factors over L
have degree 1
.
Main definitions #
polynomial.splits i f
: A predicate on a homomorphismi : K →+* L
from a commutative ring to a field and a polynomialf
saying thatf.map i
is zero or all of its irreducible factors overL
have degree1
.
Main statements #
lift_of_splits
: IfK
andL
are field extensions of a fieldF
and for some finite subsetS
ofK
, the minimal polynomial of everyx ∈ K
splits as a polynomial with coefficients inL
, thenalgebra.adjoin F S
embeds intoL
.
A polynomial splits
iff it is zero or all of its irreducible factors have degree
1.
Equations
- polynomial.splits i f = (polynomial.map i f = 0 ∨ ∀ {g : polynomial L}, irreducible g → g ∣ polynomial.map i f → g.degree = 1)
Pick a root of a polynomial that splits. See root_of_splits
for polynomials over a field
which has simpler assumptions.
Equations
- polynomial.root_of_splits' i hf hfd = classical.some _
This lemma is for polynomials over a field.
This lemma is for polynomials over a field.
Pick a root of a polynomial that splits. This version is for polynomials over a field and has simpler assumptions.
Equations
- polynomial.root_of_splits i hf hfd = polynomial.root_of_splits' i hf _
root_of_splits'
is definitionally equal to root_of_splits
.
A polynomial splits if and only if it has as many roots as its degree.
If P
is a monic polynomial that splits, then coeff P 0
equals the product of the roots.
If P
is a monic polynomial that splits, then P.next_coeff
equals the sum of the roots.