Rational root theorem and integral root theorem #
This file contains the rational root theorem and integral root theorem.
The rational root theorem for a unique factorization domain A
with localization S, states that the roots of p : polynomial A in A's
field of fractions are of the form x / y with x y : A, x ∣ p.coeff 0 and
y ∣ p.leading_coeff.
The corollary is the integral root theorem is_integer_of_is_root_of_monic:
if p is monic, its roots must be integers.
Finally, we use this to show unique factorization domains are integrally closed.
References #
Rational root theorem part 1:
if r : f.codomain is a root of a polynomial over the ufd A,
then the numerator of r divides the constant coefficient
Rational root theorem part 2:
if r : f.codomain is a root of a polynomial over the ufd A,
then the denominator of r divides the leading coefficient
Integral root theorem:
if r : f.codomain is a root of a monic polynomial over the ufd A,
then r is an integer