Commit 2020-07-03 23:00 742dc887

feat(ring_theory/polynomial): rational root theorem and integral root theorem (#3241) Prove the rational root theorem for a unique factorization domain A: Let K be the field of fractions of A and p a polynomial over A. If x : K is a root of p, then the numerator of x divides the constant coefficient and the denominator of x divides the leading coefficient. (This required defining the numerator and denominator.) As a corollary we have the integral root theorem: if p is monic, then its roots in K are in fact elements of A. As a second corollary, the integral closure of A in K is A itself.