# Rational root theorem and integral root theorem #

This file contains the rational root theorem and integral root theorem. The rational root theorem (`num_dvd_of_is_root` and `den_dvd_of_is_root`) 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 #

- https://en.wikipedia.org/wiki/Rational_root_theorem

source
theorem scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero {A : Type u_1} {S : Type u_4} [CommRing A] [CommRing S] {M : Submonoid A} [Algebra A S] [IsLocalization M S] {p : Polynomial A} {r : A} {s : ↥M} (hr : (Polynomial.aeval (IsLocalization.mk' S r s)) p = 0) :
(Polynomial.aeval ((algebraMap A S) r)) (p.scaleRoots ↑s) = 0
source
theorem num_isRoot_scaleRoots_of_aeval_eq_zero {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDomain A] [UniqueFactorizationMonoid A] {p : Polynomial A} {x : K} (hr : (Polynomial.aeval x) p = 0) :
(p.scaleRoots ↑(IsFractionRing.den A x)).IsRoot (IsFractionRing.num A x)
source
theorem num_dvd_of_is_root {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} {r : K} (hr : (Polynomial.aeval r) p = 0) :
IsFractionRing.num A r ∣ 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

source
theorem den_dvd_of_is_root {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} {r : K} (hr : (Polynomial.aeval r) p = 0) :
↑(IsFractionRing.den A r) ∣ p.leadingCoeff

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

source
theorem isInteger_of_is_root_of_monic {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} (hp : p.Monic) {r : K} (hr : (Polynomial.aeval r) p = 0) :
IsLocalization.IsInteger A r

Integral root theorem: if `r : f.codomain` is a root of a monic polynomial over the ufd `A`, then `r` is an integer

source
theorem exists_integer_of_is_root_of_monic {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {p : Polynomial A} (hp : p.Monic) {r : K} (hr : (Polynomial.aeval r) p = 0) :
∃ (r' : A), r = (algebraMap A K) r' ∧ r' ∣ p.coeff 0
source
theorem UniqueFactorizationMonoid.integer_of_integral {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [Field K] [Algebra A K] [IsFractionRing A K] {x : K} :
IsIntegral A x → IsLocalization.IsInteger A x
source
@[instance 100]
instance UniqueFactorizationMonoid.instIsIntegrallyClosed {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] :
IsIntegrallyClosed A