Rational root theorem and integral root theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.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 #

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

source

theorem scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero {A : Type u_1} {S : Type u_4} [comm_ring A] [comm_ring S] {M : submonoid A} [algebra A S] [is_localization M S] {p : polynomial A} {r : A} {s : ↥M} (hr : ⇑(polynomial.aeval (is_localization.mk' S r s)) p = 0) :

⇑(polynomial.aeval (⇑(algebra_map A S) r)) (p.scale_roots ↑s) = 0

source

theorem num_is_root_scale_roots_of_aeval_eq_zero {A : Type u_1} {K : Type u_2} [comm_ring A] [field K] [algebra A K] [is_fraction_ring A K] [is_domain A] [unique_factorization_monoid A] {p : polynomial A} {x : K} (hr : ⇑(polynomial.aeval x) p = 0) :

(p.scale_roots ↑(is_fraction_ring.denom A x)).is_root (is_fraction_ring.num A x)

source

theorem num_dvd_of_is_root {A : Type u_1} {K : Type u_2} [comm_ring A] [is_domain A] [unique_factorization_monoid A] [field K] [algebra A K] [is_fraction_ring A K] {p : polynomial A} {r : K} (hr : ⇑(polynomial.aeval r) p = 0) :

is_fraction_ring.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 denom_dvd_of_is_root {A : Type u_1} {K : Type u_2} [comm_ring A] [is_domain A] [unique_factorization_monoid A] [field K] [algebra A K] [is_fraction_ring A K] {p : polynomial A} {r : K} (hr : ⇑(polynomial.aeval r) p = 0) :

↑(is_fraction_ring.denom A r) ∣ p.leading_coeff

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 is_integer_of_is_root_of_monic {A : Type u_1} {K : Type u_2} [comm_ring A] [is_domain A] [unique_factorization_monoid A] [field K] [algebra A K] [is_fraction_ring A K] {p : polynomial A} (hp : p.monic) {r : K} (hr : ⇑(polynomial.aeval r) p = 0) :

is_localization.is_integer 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 unique_factorization_monoid.integer_of_integral {A : Type u_1} {K : Type u_2} [comm_ring A] [is_domain A] [unique_factorization_monoid A] [field K] [algebra A K] [is_fraction_ring A K] {x : K} :

is_integral A x → is_localization.is_integer A x

source

@[protected, instance]

def unique_factorization_monoid.is_integrally_closed {A : Type u_1} [comm_ring A] [is_domain A] [unique_factorization_monoid A] :

is_integrally_closed A