mathlibdocumentation

ring_theory.polynomial.rational_root

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 #

theorem scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero {A : Type u_1} {S : Type u_4} [comm_ring S] {M : submonoid A} {f : S} {p : polynomial A} {r : A} {s : M} (hr : (polynomial.aeval (f.mk' r s)) p = 0) :
theorem num_is_root_scale_roots_of_aeval_eq_zero {A : Type u_1} {K : Type u_2} [field K] (g : K) {p : polynomial A} (hr : p = 0) :
(g.denom x)).is_root (g.num x)
theorem num_dvd_of_is_root {A : Type u_1} {K : Type u_2} [field K] {f : K} {p : polynomial A} (hr : p = 0) :
f.num 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

theorem denom_dvd_of_is_root {A : Type u_1} {K : Type u_2} [field K] {f : K} {p : polynomial A} (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

theorem is_integer_of_is_root_of_monic {A : Type u_1} {K : Type u_2} [field K] {f : K} {p : polynomial A} (hp : p.monic) (hr : p = 0) :

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

theorem unique_factorization_monoid.integer_of_integral {A : Type u_1} {K : Type u_2} [field K] {f : K}  :
theorem unique_factorization_monoid.integrally_closed {A : Type u_1} {K : Type u_2} [field K] {f : K} :