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

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

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)) (Polynomial.scaleRoots p ↑s) = 0

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) : Polynomial.IsRoot (Polynomial.scaleRoots p ↑(IsFractionRing.den A x)) (IsFractionRing.num A x)

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 ∣ Polynomial.coeff p 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} [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) ∣ Polynomial.leadingCoeff p

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

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 : Polynomial.Monic p) {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

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

instance UniqueFactorizationMonoid.instIsIntegrallyClosed {A : Type u_1} [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] : IsIntegrallyClosed A

Equations

• (_ : IsIntegrallyClosed A) = (_ : IsIntegrallyClosed A)