Theory of univariate polynomials #
This file starts looking like the ring theory of $ R[X] $
_ %ₘ q
as an R
-linear map.
Equations
- q.mod_by_monic_hom = {to_fun := λ (p : polynomial R), p %ₘ q, map_add' := _, map_smul' := _}
This lemma is useful for working with the int_degree
of a rational function.
The multiplicity of a
as root of (X - a) ^ n
is n
.
If (X - a) ^ n
divides a polynomial p
then the multiplicity of a
as root of p
is at
least n
.
The multiplicity of p + q
is at least the minimum of the multiplicities.
roots p
noncomputably gives a multiset containing all the roots of p
,
including their multiplicities.
nth_roots n a
noncomputably returns the solutions to x ^ n = a
Equations
- polynomial.nth_roots n a = (polynomial.X ^ n - ⇑polynomial.C a).roots
The multiset nth_roots ↑n (1 : R)
as a finset.
Equations
The set of distinct roots of p
in E
.
If you have a non-separable polynomial, use polynomial.roots
for the multiset
where multiple roots have the appropriate multiplicity.
Equations
- p.root_set S = ↑((polynomial.map (algebra_map T S) p).roots.to_finset)
Instances for ↥polynomial.root_set
Equations
- p.root_set_fintype S = finset_coe.fintype (polynomial.map (algebra_map T S) p).roots.to_finset
Division by a monic polynomial doesn't change the leading coefficient.
The product ∏ (X - a)
for a
inside the multiset p.roots
divides p
.
A polynomial p
that has as many roots as its degree
can be written p = p.leading_coeff * ∏(X - a)
, for a
in p.roots
.
A monic polynomial p
that has as many roots as its degree
can be written p = ∏(X - a)
, for a
in p.roots
.
A polynomial over an integral domain R
is irreducible if it is monic and
irreducible after mapping into an integral domain S
.
A special case of this lemma is that a polynomial over ℤ
is irreducible if
it is monic and irreducible over ℤ/pℤ
for some prime p
.