16.4. Roots
A point r is a root of p when p.eval r = 0.
This is recorded as Polynomial.IsRoot, with named unfolding lemma
Polynomial.IsRoot.def:
example : p.IsRoot r ↔ p.eval r = 0 := IsRoot.def
16.4.1. Multiset of roots in the coefficient ring
Over a commutative ring that is a domain, the multiset of roots of p,
counted with multiplicity, is Polynomial.roots:
#check (p.roots : Multiset R)
By convention, Polynomial.roots_zero says ((0 : R[X]).roots : Multiset R) = 0
(the empty multiset), even though every element of R is a root of the zero
polynomial in the usual mathematical sense.
This convention keeps statements like Polynomial.roots_mul clean.
The cardinality of roots is bounded by the degree:
see Polynomial.card_roots and Polynomial.card_roots'.
16.4.2. Roots in an extension
When the roots of (p : R[X]) should be sought in a (commutative-ring, domain)
R-algebra S rather than in R itself,
Polynomial.aroots returns them as a Multiset S:
#check (p.aroots S : Multiset S)
The underlying set (without multiplicities) is Polynomial.rootSet:
#check (p.rootSet S : Set S)
By definition, Polynomial.aroots is the roots of p.map (algebraMap R S),
and Polynomial.rootSet is the coercion of that multiset to a set
(see Polynomial.aroots_def and Polynomial.rootSet_def).