# 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 : A[X] in A's field of fractions are of the form x / y with x y : A, x ∣ p.coeff 0 and y ∣ p.leadingCoeff. The corollary is the integral root theorem isInteger_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 #

theorem scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero {A : Type u_1} {S : Type u_4} [] [] {M : } [Algebra A S] [] {p : } {r : A} {s : M} (hr : () p = 0) :
(Polynomial.aeval (() r)) (p.scaleRoots s) = 0
theorem num_isRoot_scaleRoots_of_aeval_eq_zero {A : Type u_1} {K : Type u_2} [] [] [Algebra A K] [] [] {p : } {x : K} (hr : () p = 0) :
(p.scaleRoots ()).IsRoot ()
theorem num_dvd_of_is_root {A : Type u_1} {K : Type u_2} [] [] [] [Algebra A K] [] {p : } {r : K} (hr : () p = 0) :
p.coeff 0

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

theorem den_dvd_of_is_root {A : Type u_1} {K : Type u_2} [] [] [] [Algebra A K] [] {p : } {r : K} (hr : () p = 0) :
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