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
- https://en.wikipedia.org/wiki/Rational_root_theorem
scale_roots p s is a polynomial with root r * s for each root r of p.
Equations
- scale_roots p s = finsupp.on_finset p.support (λ (i : ℕ), p.coeff i * s ^ (p.nat_degree - i)) _
@[simp]
theorem
coeff_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R)
(i : ℕ) :
(scale_roots p s).coeff i = p.coeff i * s ^ (p.nat_degree - i)
theorem
coeff_scale_roots_nat_degree
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(scale_roots p s).coeff p.nat_degree = p.leading_coeff
theorem
scale_roots_ne_zero
{R : Type u_3}
[comm_ring R]
{p : polynomial R}
(hp : p ≠ 0)
(s : R) :
scale_roots p s ≠ 0
theorem
support_scale_roots_le
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(scale_roots p s).support ≤ p.support
theorem
support_scale_roots_eq
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
{s : R} :
s ∈ non_zero_divisors R → (scale_roots p s).support = p.support
@[simp]
theorem
degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
{s : R} :
(scale_roots p s).degree = p.degree
@[simp]
theorem
nat_degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(scale_roots p s).nat_degree = p.nat_degree
theorem
monic_scale_roots_iff
{R : Type u_3}
[comm_ring R]
{p : polynomial R}
(s : R) :
(scale_roots p s).monic ↔ p.monic
theorem
scale_roots_eval₂_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
{p : polynomial S}
(f : S →+* R)
{r : R}
{s : S} :
polynomial.eval₂ f r p = 0 → s ∈ non_zero_divisors S → polynomial.eval₂ f (⇑f s * r) (scale_roots p s) = 0
theorem
scale_roots_aeval_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
[algebra S R]
{p : polynomial S}
{r : R}
{s : S} :
⇑(polynomial.aeval r) p = 0 → s ∈ non_zero_divisors S → ⇑(polynomial.aeval (⇑(algebra_map S R) s * r)) (scale_roots p s) = 0
theorem
scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[field K]
{p : polynomial A}
{f : A →+* K}
(hf : function.injective ⇑f)
{r s : A} :
polynomial.eval₂ f (⇑f r / ⇑f s) p = 0 → s ∈ non_zero_divisors A → polynomial.eval₂ f (⇑f r) (scale_roots p s) = 0
theorem
scale_roots_aeval_eq_zero_of_aeval_div_eq_zero
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[field K]
[algebra A K]
(inj : function.injective ⇑(algebra_map A K))
{p : polynomial A}
{r s : A} :
⇑(polynomial.aeval (⇑(algebra_map A K) r / ⇑(algebra_map A K) s)) p = 0 → s ∈ non_zero_divisors A → ⇑(polynomial.aeval (⇑(algebra_map A K) r)) (scale_roots p s) = 0
theorem
scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero
{A : Type u_1}
{S : Type u_4}
[integral_domain A]
[comm_ring S]
{M : submonoid A}
{f : localization_map M S}
{p : polynomial A}
{r : A}
{s : ↥M} :
⇑(polynomial.aeval (f.mk' r s)) p = 0 → M ≤ non_zero_divisors A → ⇑(polynomial.aeval (⇑(f.to_map) r)) (scale_roots p ↑s) = 0
theorem
num_is_root_scale_roots_of_aeval_eq_zero
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[field K]
[unique_factorization_domain A]
(g : fraction_map A K)
{p : polynomial A}
{x : localization_map.codomain g} :
⇑(polynomial.aeval x) p = 0 → (scale_roots p ↑(g.denom x)).is_root (g.num x)
theorem
num_dvd_of_is_root
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[unique_factorization_domain A]
[field K]
{f : fraction_map A K}
{p : polynomial A}
{r : localization_map.codomain f} :
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}
[integral_domain A]
[unique_factorization_domain A]
[field K]
{f : fraction_map A K}
{p : polynomial A}
{r : localization_map.codomain f} :
⇑(polynomial.aeval r) p = 0 → ↑(f.denom 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
theorem
is_integer_of_is_root_of_monic
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[unique_factorization_domain A]
[field K]
{f : fraction_map A K}
{p : polynomial A}
(hp : p.monic)
{r : localization_map.codomain f} :
⇑(polynomial.aeval r) p = 0 → localization_map.is_integer f 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
unique_factorization_domain.integer_of_integral
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[unique_factorization_domain A]
[field K]
{f : fraction_map A K}
{x : localization_map.codomain f} :
is_integral A x → localization_map.is_integer f x
theorem
unique_factorization_domain.integrally_closed
{A : Type u_1}
{K : Type u_2}
[integral_domain A]
[unique_factorization_domain A]
[field K]
{f : fraction_map A K} :