mathlib documentation

data.polynomial.ring_division

Theory of univariate polynomials #

This file starts looking like the ring theory of $ R[X] $

Main definitions #

Main statements #

source
theorem polynomial.nat_degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [semiring S] [algebra R S] {p : polynomial R} (hp : p ≠ 0) {z : S} (hz : ⇑(polynomial.aeval z) p = 0) (inj : ∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) :
0 < p.nat_degree
source
theorem polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [semiring S] [algebra R S] {p : polynomial R} (hp : p ≠ 0) {z : S} (hz : ⇑(polynomial.aeval z) p = 0) (inj : ∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) :
0 < p.degree
source
theorem polynomial.mod_by_monic_eq_of_dvd_sub {R : Type u} [comm_ring R] {q : polynomial R} (hq : q.monic) {p₁ p₂ : polynomial R} (h : q ∣ p₁ - p₂) :
p₁ %ₘ q = p₂ %ₘ q
source
theorem polynomial.add_mod_by_monic {R : Type u} [comm_ring R] {q : polynomial R} (p₁ p₂ : polynomial R) :
(p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
source
theorem polynomial.smul_mod_by_monic {R : Type u} [comm_ring R] {q : polynomial R} (c : R) (p : polynomial R) :
c • p %ₘ q = c • (p %ₘ q)
source
noncomputable def polynomial.mod_by_monic_hom {R : Type u} [comm_ring R] (q : polynomial R) :
polynomial R →ₗ[R] polynomial R

_ %ₘ q as an R-linear map.

Equations
source
@[simp]
theorem polynomial.mod_by_monic_hom_apply {R : Type u} [comm_ring R] (q p : polynomial R) :
⇑(q.mod_by_monic_hom) p = p %ₘ q
source
theorem polynomial.aeval_mod_by_monic_eq_self_of_root {R : Type u} {S : Type v} [comm_ring R] [ring S] [algebra R S] {p q : polynomial R} (hq : q.monic) {x : S} (hx : ⇑(polynomial.aeval x) q = 0) :
⇑(polynomial.aeval x) (p %ₘ q) = ⇑(polynomial.aeval x) p
source
@[protected, instance]
def polynomial.no_zero_divisors {R : Type u} [semiring R] [no_zero_divisors R] :
no_zero_divisors (polynomial R)
source
theorem polynomial.nat_degree_mul {R : Type u} [semiring R] [no_zero_divisors R] {p q : polynomial R} (hp : p ≠ 0) (hq : q ≠ 0) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
source
theorem polynomial.trailing_degree_mul {R : Type u} [semiring R] [no_zero_divisors R] {p q : polynomial R} :
(p * q).trailing_degree = p.trailing_degree + q.trailing_degree
source
@[simp]
theorem polynomial.nat_degree_pow {R : Type u} [semiring R] [no_zero_divisors R] (p : polynomial R) (n : ℕ) :
(p ^ n).nat_degree = n * p.nat_degree
source
theorem polynomial.degree_le_mul_left {R : Type u} [semiring R] [no_zero_divisors R] {q : polynomial R} (p : polynomial R) (hq : q ≠ 0) :
p.degree ≤ (p * q).degree
source
theorem polynomial.nat_degree_le_of_dvd {R : Type u} [semiring R] [no_zero_divisors R] {p q : polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) :
p.nat_degree ≤ q.nat_degree
source
theorem polynomial.degree_le_of_dvd {R : Type u} [semiring R] [no_zero_divisors R] {p q : polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) :
p.degree ≤ q.degree
source
theorem polynomial.nat_degree_sub_eq_of_prod_eq {R : Type u} [semiring R] [no_zero_divisors R] {p₁ p₂ q₁ q₂ : polynomial R} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0) (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
↑(p₁.nat_degree) - ↑(q₁.nat_degree) = ↑(p₂.nat_degree) - ↑(q₂.nat_degree)

This lemma is useful for working with the int_degree of a rational function.

source
theorem polynomial.nat_degree_eq_zero_of_is_unit {R : Type u} [semiring R] [no_zero_divisors R] {p : polynomial R} (h : is_unit p) :
p.nat_degree = 0
source
theorem polynomial.degree_eq_zero_of_is_unit {R : Type u} [semiring R] [no_zero_divisors R] {p : polynomial R} [nontrivial R] (h : is_unit p) :
p.degree = 0
source
theorem polynomial.is_unit_iff {R : Type u} [semiring R] [no_zero_divisors R] {p : polynomial R} :
is_unit p ↔ ∃ (r : R), is_unit r ∧ ⇑polynomial.C r = p
source
@[simp]
theorem polynomial.degree_bit0_eq {R : Type u} [semiring R] [no_zero_divisors R] [char_zero R] (p : polynomial R) :
(bit0 p).degree = p.degree
source
@[simp]
theorem polynomial.nat_degree_bit0_eq {R : Type u} [semiring R] [no_zero_divisors R] [char_zero R] (p : polynomial R) :
(bit0 p).nat_degree = p.nat_degree
source
@[simp]
theorem polynomial.nat_degree_bit1_eq {R : Type u} [semiring R] [no_zero_divisors R] [char_zero R] (p : polynomial R) :
(bit1 p).nat_degree = p.nat_degree
source
theorem polynomial.degree_bit1_eq {R : Type u} [semiring R] [no_zero_divisors R] [char_zero R] {p : polynomial R} (hp : 0 < p.degree) :
(bit1 p).degree = p.degree
source
theorem polynomial.irreducible_of_monic {R : Type u} [comm_semiring R] [no_zero_divisors R] {p : polynomial R} (hp : p.monic) (hp1 : p ≠ 1) :
irreducible p ↔ ∀ (f g : polynomial R), f.monic → g.monic → f * g = p → f = 1 ∨ g = 1
source
theorem polynomial.root_mul {R : Type u} {a : R} [comm_semiring R] [no_zero_divisors R] {p q : polynomial R} :
(p * q).is_root a ↔ p.is_root a ∨ q.is_root a
source
theorem polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [comm_semiring R] [no_zero_divisors R] {p q : polynomial R} (h : (p * q).is_root a) :
p.is_root a ∨ q.is_root a
source
@[protected, instance]
def polynomial.is_domain {R : Type u} [ring R] [is_domain R] :
is_domain (polynomial R)
source
theorem polynomial.le_root_multiplicity_iff {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p ≠ 0) {a : R} {n : ℕ} :
n ≤ polynomial.root_multiplicity a p ↔ (polynomial.X - ⇑polynomial.C a) ^ n ∣ p

The multiplicity of a as root of a nonzero polynomial p is at least n iff (X - a) ^ n divides p.

source
theorem polynomial.root_multiplicity_le_iff {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p ≠ 0) (a : R) (n : ℕ) :
polynomial.root_multiplicity a p ≤ n ↔ ¬(polynomial.X - ⇑polynomial.C a) ^ (n + 1) ∣ p
source
theorem polynomial.pow_root_multiplicity_not_dvd {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p ≠ 0) (a : R) :
¬(polynomial.X - ⇑polynomial.C a) ^ (polynomial.root_multiplicity a p + 1) ∣ p
source
theorem polynomial.root_multiplicity_add {R : Type u} [comm_ring R] {p q : polynomial R} (a : R) (hzero : p + q ≠ 0) :
linear_order.min (polynomial.root_multiplicity a p) (polynomial.root_multiplicity a q) ≤ polynomial.root_multiplicity a (p + q)

The multiplicity of p + q is at least the minimum of the multiplicities.

source
@[simp]
theorem polynomial.degree_coe_units {R : Type u} [comm_ring R] [is_domain R] (u : (polynomial R)ˣ) :
↑u.degree = 0
source
theorem polynomial.prime_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
prime (polynomial.X - ⇑polynomial.C r)
source
theorem polynomial.prime_X {R : Type u} [comm_ring R] [is_domain R] :
prime polynomial.X
source
theorem polynomial.monic.prime_of_degree_eq_one {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp1 : p.degree = 1) (hm : p.monic) :
prime p
source
theorem polynomial.irreducible_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
irreducible (polynomial.X - ⇑polynomial.C r)
source
theorem polynomial.irreducible_X {R : Type u} [comm_ring R] [is_domain R] :
irreducible polynomial.X
source
theorem polynomial.monic.irreducible_of_degree_eq_one {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp1 : p.degree = 1) (hm : p.monic) :
irreducible p
source
theorem polynomial.eq_of_monic_of_associated {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (hpq : associated p q) :
p = q
source
theorem polynomial.root_multiplicity_mul {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} {x : R} (hpq : p * q ≠ 0) :
polynomial.root_multiplicity x (p * q) = polynomial.root_multiplicity x p + polynomial.root_multiplicity x q
source
theorem polynomial.root_multiplicity_X_sub_C_self {R : Type u} [comm_ring R] [is_domain R] {x : R} :
polynomial.root_multiplicity x (polynomial.X - ⇑polynomial.C x) = 1
source
theorem polynomial.root_multiplicity_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {x y : R} :
polynomial.root_multiplicity x (polynomial.X - ⇑polynomial.C y) = ite (x = y) 1 0
source
theorem polynomial.root_multiplicity_X_sub_C_pow {R : Type u} [comm_ring R] [is_domain R] (a : R) (n : ℕ) :
polynomial.root_multiplicity a ((polynomial.X - ⇑polynomial.C a) ^ n) = n

The multiplicity of a as root of (X - a) ^ n is n.

source
theorem polynomial.exists_multiset_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p ≠ 0) :
∃ (s : multiset R), ↑(⇑multiset.card s) ≤ p.degree ∧ ∀ (a : R), multiset.count a s = polynomial.root_multiplicity a p
source
noncomputable def polynomial.roots {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
multiset R

roots p noncomputably gives a multiset containing all the roots of p, including their multiplicities.

Equations
source
@[simp]
theorem polynomial.roots_zero {R : Type u} [comm_ring R] [is_domain R] :
0.roots = 0
source
theorem polynomial.card_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp0 : p ≠ 0) :
↑(⇑multiset.card p.roots) ≤ p.degree
source
theorem polynomial.card_roots' {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
⇑multiset.card p.roots ≤ p.nat_degree
source
theorem polynomial.card_roots_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a : R} (hp0 : 0 < p.degree) :
↑(⇑multiset.card (p - ⇑polynomial.C a).roots) ≤ p.degree
source
theorem polynomial.card_roots_sub_C' {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a : R} (hp0 : 0 < p.degree) :
⇑multiset.card (p - ⇑polynomial.C a).roots ≤ p.nat_degree
source
@[simp]
theorem polynomial.count_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] (p : polynomial R) :
multiset.count a p.roots = polynomial.root_multiplicity a p
source
@[simp]
theorem polynomial.mem_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p ≠ 0) :
a ∈ p.roots ↔ p.is_root a
source
theorem polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] {p : polynomial R} (h : a ∈ p.roots) :
p ≠ 0
source
theorem polynomial.is_root_of_mem_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] {p : polynomial R} (h : a ∈ p.roots) :
p.is_root a
source
theorem polynomial.card_le_degree_of_subset_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {Z : finset R} (h : Z.val ⊆ p.roots) :
Z.card ≤ p.nat_degree
source
theorem polynomial.finite_set_of_is_root {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p ≠ 0) :
{x : R | p.is_root x}.finite
source
theorem polynomial.eq_zero_of_infinite_is_root {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) (h : {x : R | p.is_root x}.infinite) :
p = 0
source
theorem polynomial.exists_max_root {R : Type u} [comm_ring R] [is_domain R] [linear_order R] (p : polynomial R) (hp : p ≠ 0) :
∃ (x₀ : R), ∀ (x : R), p.is_root x → x ≤ x₀
source
theorem polynomial.exists_min_root {R : Type u} [comm_ring R] [is_domain R] [linear_order R] (p : polynomial R) (hp : p ≠ 0) :
∃ (x₀ : R), ∀ (x : R), p.is_root x → x₀ ≤ x
source
theorem polynomial.eq_of_infinite_eval_eq {R : Type u} [comm_ring R] [is_domain R] (p q : polynomial R) (h : {x : R | polynomial.eval x p = polynomial.eval x q}.infinite) :
p = q
source
theorem polynomial.roots_mul {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (hpq : p * q ≠ 0) :
(p * q).roots = p.roots + q.roots
source
theorem polynomial.roots.le_of_dvd {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (h : q ≠ 0) :
p ∣ q → p.roots ≤ q.roots
source
@[simp]
theorem polynomial.mem_roots_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a x : R} (hp0 : 0 < p.degree) :
x ∈ (p - ⇑polynomial.C a).roots ↔ polynomial.eval x p = a
source
@[simp]
theorem polynomial.roots_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
(polynomial.X - ⇑polynomial.C r).roots = {r}
source
@[simp]
theorem polynomial.roots_X {R : Type u} [comm_ring R] [is_domain R] :
polynomial.X.roots = {0}
source
@[simp]
theorem polynomial.roots_C {R : Type u} [comm_ring R] [is_domain R] (x : R) :
(⇑polynomial.C x).roots = 0
source
@[simp]
theorem polynomial.roots_one {R : Type u} [comm_ring R] [is_domain R] :
1.roots = ∅
source
@[simp]
theorem polynomial.roots_C_mul {R : Type u} {a : R} [comm_ring R] [is_domain R] (p : polynomial R) (ha : a ≠ 0) :
(⇑polynomial.C a * p).roots = p.roots
source
@[simp]
theorem polynomial.roots_smul_nonzero {R : Type u} {a : R} [comm_ring R] [is_domain R] (p : polynomial R) (ha : a ≠ 0) :
(a • p).roots = p.roots
source
theorem polynomial.roots_list_prod {R : Type u} [comm_ring R] [is_domain R] (L : list (polynomial R)) :
0 ∉ L → L.prod.roots = ↑L.bind polynomial.roots
source
theorem polynomial.roots_multiset_prod {R : Type u} [comm_ring R] [is_domain R] (m : multiset (polynomial R)) :
0 ∉ m → m.prod.roots = m.bind polynomial.roots
source
theorem polynomial.roots_prod {R : Type u} [comm_ring R] [is_domain R] {ι : Type u_1} (f : ι → polynomial R) (s : finset ι) :
s.prod f ≠ 0 → (s.prod f).roots = s.val.bind (λ (i : ι), (f i).roots)
source
@[simp]
theorem polynomial.roots_pow {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) (n : ℕ) :
(p ^ n).roots = n • p.roots
source
theorem polynomial.roots_X_pow {R : Type u} [comm_ring R] [is_domain R] (n : ℕ) :
(polynomial.X ^ n).roots = n • {0}
source
theorem polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [comm_ring R] [is_domain R] (ha : a ≠ 0) (n : ℕ) :
(⇑polynomial.C a * polynomial.X ^ n).roots = n • {0}
source
@[simp]
theorem polynomial.roots_monomial {R : Type u} {a : R} [comm_ring R] [is_domain R] (ha : a ≠ 0) (n : ℕ) :
(⇑(polynomial.monomial n) a).roots = n • {0}
source
theorem polynomial.roots_prod_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (s : finset R) :
(s.prod (λ (a : R), polynomial.X - ⇑polynomial.C a)).roots = s.val
source
@[simp]
theorem polynomial.roots_multiset_prod_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (s : multiset R) :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) s).prod.roots = s
source
@[simp]
theorem polynomial.nat_degree_multiset_prod_X_sub_C_eq_card {R : Type u} [comm_ring R] [is_domain R] (s : multiset R) :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) s).prod.nat_degree = ⇑multiset.card s
source
theorem polynomial.card_roots_X_pow_sub_C {R : Type u} [comm_ring R] [is_domain R] {n : ℕ} (hn : 0 < n) (a : R) :
⇑multiset.card (polynomial.X ^ n - ⇑polynomial.C a).roots ≤ n
source
noncomputable def polynomial.nth_roots {R : Type u} [comm_ring R] [is_domain R] (n : ℕ) (a : R) :
multiset R

nth_roots n a noncomputably returns the solutions to x ^ n = a

Equations
source
@[simp]
theorem polynomial.mem_nth_roots {R : Type u} [comm_ring R] [is_domain R] {n : ℕ} (hn : 0 < n) {a x : R} :
x ∈ polynomial.nth_roots n a ↔ x ^ n = a
source
@[simp]
theorem polynomial.nth_roots_zero {R : Type u} [comm_ring R] [is_domain R] (r : R) :
polynomial.nth_roots 0 r = 0
source
theorem polynomial.card_nth_roots {R : Type u} [comm_ring R] [is_domain R] (n : ℕ) (a : R) :
⇑multiset.card (polynomial.nth_roots n a) ≤ n
source
@[simp]
theorem polynomial.nth_roots_two_eq_zero_iff {R : Type u} [comm_ring R] [is_domain R] {r : R} :
polynomial.nth_roots 2 r = 0 ↔ ¬is_square r
source
noncomputable def polynomial.nth_roots_finset (n : ℕ) (R : Type u_1) [comm_ring R] [is_domain R] :
finset R

The multiset nth_roots ↑n (1 : R) as a finset.

Equations
source
@[simp]
theorem polynomial.mem_nth_roots_finset {R : Type u} [comm_ring R] [is_domain R] {n : ℕ} (h : 0 < n) {x : R} :
x ∈ polynomial.nth_roots_finset n R ↔ x ^ n = 1
source
@[simp]
theorem polynomial.nth_roots_finset_zero {R : Type u} [comm_ring R] [is_domain R] :
polynomial.nth_roots_finset 0 R = ∅
source
theorem polynomial.monic.comp {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (h : q.nat_degree ≠ 0) :
(p.comp q).monic
source
theorem polynomial.monic.comp_X_add_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) (r : R) :
(p.comp (polynomial.X + ⇑polynomial.C r)).monic
source
theorem polynomial.monic.comp_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) (r : R) :
(p.comp (polynomial.X - ⇑polynomial.C r)).monic
source
theorem polynomial.units_coeff_zero_smul {R : Type u} [comm_ring R] [is_domain R] (c : (polynomial R)ˣ) (p : polynomial R) :
↑c.coeff 0 • p = ↑c * p
source
@[simp]
theorem polynomial.nat_degree_coe_units {R : Type u} [comm_ring R] [is_domain R] (u : (polynomial R)ˣ) :
↑u.nat_degree = 0
source
theorem polynomial.comp_eq_zero_iff {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} :
p.comp q = 0 ↔ p = 0 ∨ polynomial.eval (q.coeff 0) p = 0 ∧ q = ⇑polynomial.C (q.coeff 0)
source
theorem polynomial.zero_of_eval_zero {R : Type u} [comm_ring R] [is_domain R] [infinite R] (p : polynomial R) (h : ∀ (x : R), polynomial.eval x p = 0) :
p = 0
source
theorem polynomial.funext {R : Type u} [comm_ring R] [is_domain R] [infinite R] {p q : polynomial R} (ext : ∀ (r : R), polynomial.eval r p = polynomial.eval r q) :
p = q
source
def polynomial.root_set {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [algebra T S] :
set S

The set of distinct roots of p in E.

If you have a non-separable polynomial, use polynomial.roots for the multiset where multiple roots have the appropriate multiplicity.

Equations
Instances for ↥polynomial.root_set
source
theorem polynomial.root_set_def {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [algebra T S] :
p.root_set S = ↑((polynomial.map (algebra_map T S) p).roots.to_finset)
source
@[simp]
theorem polynomial.root_set_C {S : Type v} {T : Type w} [comm_ring T] [comm_ring S] [is_domain S] [algebra T S] (a : T) :
(⇑polynomial.C a).root_set S = ∅
source
@[simp]
theorem polynomial.root_set_zero {T : Type w} [comm_ring T] (S : Type u_1) [comm_ring S] [is_domain S] [algebra T S] :
0.root_set S = ∅
source
@[protected, instance]
noncomputable def polynomial.root_set_fintype {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [algebra T S] :
fintype ↥(p.root_set S)
Equations
source
theorem polynomial.root_set_finite {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [algebra T S] :
(p.root_set S).finite
source
theorem polynomial.bUnion_roots_finite {R : Type u_1} {S : Type u_2} [semiring R] [comm_ring S] [is_domain S] (m : R →+* S) (d : ℕ) {U : set R} (h : U.finite) :
(⋃ (f : polynomial R) (hf : f.nat_degree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑((polynomial.map m f).roots.to_finset)).finite

The set of roots of all polynomials of bounded degree and having coefficients in a finite set is finite.

source
theorem polynomial.mem_root_set_iff' {T : Type w} [comm_ring T] {p : polynomial T} {S : Type u_1} [comm_ring S] [is_domain S] [algebra T S] (hp : polynomial.map (algebra_map T S) p ≠ 0) (a : S) :
a ∈ p.root_set S ↔ polynomial.eval a (polynomial.map (algebra_map T S) p) = 0
source
theorem polynomial.mem_root_set_iff {T : Type w} [comm_ring T] {p : polynomial T} (hp : p ≠ 0) {S : Type u_1} [comm_ring S] [is_domain S] [algebra T S] [no_zero_smul_divisors T S] (a : S) :
a ∈ p.root_set S ↔ ⇑(polynomial.aeval a) p = 0
source
theorem polynomial.root_set_maps_to {T : Type w} [comm_ring T] {p : polynomial T} {S : Type u_1} {S' : Type u_2} [comm_ring S] [is_domain S] [algebra T S] [comm_ring S'] [is_domain S'] [algebra T S'] (hp : polynomial.map (algebra_map T S') p ≠ 0) (f : S →ₐ[T] S') :
set.maps_to ⇑f (p.root_set S) (p.root_set S')
source
theorem polynomial.ne_zero_of_mem_root_set {S : Type v} {T : Type w} [comm_ring T] {p : polynomial T} [comm_ring S] [is_domain S] [algebra T S] {a : S} (h : a ∈ p.root_set S) :
p ≠ 0
source
theorem polynomial.aeval_eq_zero_of_mem_root_set {S : Type v} {T : Type w} [comm_ring T] {p : polynomial T} [comm_ring S] [is_domain S] [algebra T S] [no_zero_smul_divisors T S] {a : S} (hx : a ∈ p.root_set S) :
⇑(polynomial.aeval a) p = 0
source
theorem polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [comm_ring R] [is_domain R] (u : (polynomial R)ˣ) :
↑u.coeff 0 ≠ 0
source
theorem polynomial.degree_eq_degree_of_associated {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (h : associated p q) :
p.degree = q.degree
source
theorem polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hi : irreducible p) {x : R} (hx : p.is_root x) :
p.degree = 1
source
theorem polynomial.leading_coeff_div_by_monic_of_monic {R : Type u} [comm_ring R] {p q : polynomial R} (hmonic : q.monic) (hdegree : q.degree ≤ p.degree) :
(p /ₘ q).leading_coeff = p.leading_coeff

Division by a monic polynomial doesn't change the leading coefficient.

source
theorem polynomial.leading_coeff_div_by_monic_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) (hp : p.degree ≠ 0) (a : R) :
(p /ₘ (polynomial.X - ⇑polynomial.C a)).leading_coeff = p.leading_coeff
source
theorem polynomial.eq_leading_coeff_mul_of_monic_of_dvd_of_nat_degree_le {R : Type u_1} [comm_ring R] {p q : polynomial R} (hp : p.monic) (hdiv : p ∣ q) (hdeg : q.nat_degree ≤ p.nat_degree) :
q = ⇑polynomial.C q.leading_coeff * p
source
theorem polynomial.eq_of_monic_of_dvd_of_nat_degree_le {R : Type u_1} [comm_ring R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (hdiv : p ∣ q) (hdeg : q.nat_degree ≤ p.nat_degree) :
q = p
source
theorem polynomial.is_coprime_X_sub_C_of_is_unit_sub {R : Type u_1} [comm_ring R] {a b : R} (h : is_unit (a - b)) :
is_coprime (polynomial.X - ⇑polynomial.C a) (polynomial.X - ⇑polynomial.C b)
source
theorem polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [field K] {I : Type v} {s : I → K} (H : function.injective s) :
pairwise (is_coprime on λ (i : I), polynomial.X - ⇑polynomial.C (s i))
source
theorem polynomial.monic_prod_multiset_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod.monic
source
theorem polynomial.prod_multiset_root_eq_finset_root {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod = p.roots.to_finset.prod (λ (a : R), (polynomial.X - ⇑polynomial.C a) ^ polynomial.root_multiplicity a p)
source
theorem polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod ∣ p

The product ∏ (X - a) for a inside the multiset p.roots divides p.

source
theorem multiset.prod_X_sub_C_dvd_iff_le_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p ≠ 0) (s : multiset R) :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) s).prod ∣ p ↔ s ≤ p.roots

A Galois connection.

source
theorem polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
∃ (q : polynomial R), (multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod * q = p ∧ ⇑multiset.card p.roots + q.nat_degree = p.nat_degree ∧ q.roots = 0
source
theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hroots : ⇑multiset.card p.roots = p.nat_degree) :
⇑polynomial.C p.leading_coeff * (multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod = p

A polynomial p that has as many roots as its degree can be written p = p.leading_coeff * ∏(X - a), for a in p.roots.

source
theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) (hroots : ⇑multiset.card p.roots = p.nat_degree) :
(multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) p.roots).prod = p

A monic polynomial p that has as many roots as its degree can be written p = ∏(X - a), for a in p.roots.

source
theorem polynomial.le_root_multiplicity_map {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {p : polynomial A} {f : A →+* B} (hmap : polynomial.map f p ≠ 0) (a : A) :
polynomial.root_multiplicity a p ≤ polynomial.root_multiplicity (⇑f a) (polynomial.map f p)
source
theorem polynomial.eq_root_multiplicity_map {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {p : polynomial A} {f : A →+* B} (hf : function.injective ⇑f) (a : A) :
polynomial.root_multiplicity a p = polynomial.root_multiplicity (⇑f a) (polynomial.map f p)
source
theorem polynomial.count_map_roots {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] {p : polynomial A} {f : A →+* B} (hmap : polynomial.map f p ≠ 0) (b : B) :
multiset.count b (multiset.map ⇑f p.roots) ≤ polynomial.root_multiplicity b (polynomial.map f p)
source
theorem polynomial.count_map_roots_of_injective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] (p : polynomial A) {f : A →+* B} (hf : function.injective ⇑f) (b : B) :
multiset.count b (multiset.map ⇑f p.roots) ≤ polynomial.root_multiplicity b (polynomial.map f p)
source
theorem polynomial.map_roots_le {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] [is_domain B] {p : polynomial A} {f : A →+* B} (h : polynomial.map f p ≠ 0) :
multiset.map ⇑f p.roots ≤ (polynomial.map f p).roots
source
theorem polynomial.map_roots_le_of_injective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] [is_domain B] (p : polynomial A) {f : A →+* B} (hf : function.injective ⇑f) :
multiset.map ⇑f p.roots ≤ (polynomial.map f p).roots
source
theorem polynomial.card_roots_le_map {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] [is_domain B] {p : polynomial A} {f : A →+* B} (h : polynomial.map f p ≠ 0) :
⇑multiset.card p.roots ≤ ⇑multiset.card (polynomial.map f p).roots
source
theorem polynomial.card_roots_le_map_of_injective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] [is_domain B] {p : polynomial A} {f : A →+* B} (hf : function.injective ⇑f) :
⇑multiset.card p.roots ≤ ⇑multiset.card (polynomial.map f p).roots
source
theorem polynomial.roots_map_of_injective_of_card_eq_nat_degree {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] [is_domain A] [is_domain B] {p : polynomial A} {f : A →+* B} (hf : function.injective ⇑f) (hroots : ⇑multiset.card p.roots = p.nat_degree) :
multiset.map ⇑f p.roots = (polynomial.map f p).roots
source
theorem polynomial.is_unit_of_is_unit_leading_coeff_of_is_unit_map {R : Type u} {S : Type v} [semiring R] [comm_ring S] [is_domain S] (φ : R →+* S) {f : polynomial R} (hf : is_unit f.leading_coeff) (H : is_unit (polynomial.map φ f)) :
is_unit f
source
theorem polynomial.monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] (φ : R →+* S) (f : polynomial R) (h_mon : f.monic) (h_irr : irreducible (polynomial.map φ f)) :
irreducible f

A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S.

A special case of this lemma is that a polynomial over ℤ is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.