Split polynomials #
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
.
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)
Instances For
This is a weaker variant of Splits.comp_of_map_degree_le_one
,
but its conditions are easier to check.
Pick a root of a polynomial that splits. See rootOfSplits
for polynomials over a field
which has simpler assumptions.
Equations
- Polynomial.rootOfSplits' i hf hfd = Classical.choose ⋯
Instances For
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.rootOfSplits i hf hfd = Polynomial.rootOfSplits' i hf ⋯
Instances For
rootOfSplits'
is definitionally equal to rootOfSplits
.
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.
Alias of Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits
.
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.nextCoeff
equals the sum of the roots.