Theory of univariate polynomials #
This file starts looking like the ring theory of $ R[X] $
Equations
- polynomial.integral_domain = {add := comm_ring.add polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero polynomial.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul polynomial.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg polynomial.comm_ring, sub := comm_ring.sub polynomial.comm_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul polynomial.comm_ring, mul_assoc := _, one := comm_ring.one polynomial.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow polynomial.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
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 R S) p).roots.to_finset)
Division by a monic polynomial doesn't change the leading coefficient.
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
.
Lift evidence that is_integral_domain R
to is_integral_domain (polynomial R)
.