mathlibdocumentation

data.polynomial.ring_division

Theory of univariate polynomials #

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

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

Main definitions #

• `polynomial.roots p`: The multiset containing all the roots of `p`, including their multiplicities.
• `polynomial.root_set p E`: The set of distinct roots of `p` in an algebra `E`.

Main statements #

• `polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C`: If a polynomial has as many roots as its degree, it can be written as the product of its leading coefficient with `∏ (X - a)` where `a` ranges through its roots.
theorem polynomial.nat_degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [semiring S] [ S] {p : polynomial R} (hp : p 0) {z : S} (hz : p = 0) (inj : (x : R), S) x = 0 x = 0) :
theorem polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [semiring S] [ S] {p : polynomial R} (hp : p 0) {z : S} (hz : p = 0) (inj : (x : R), S) x = 0 x = 0) :
0 < p.degree
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
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
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)
noncomputable def polynomial.mod_by_monic_hom {R : Type u} [comm_ring R] (q : polynomial R) :

`_ %ₘ q` as an `R`-linear map.

Equations
@[simp]
theorem polynomial.aeval_mod_by_monic_eq_self_of_root {R : Type u} {S : Type v} [comm_ring R] [ring S] [ S] {p q : polynomial R} (hq : q.monic) {x : S} (hx : q = 0) :
(p %ₘ q) = p
@[protected, instance]
theorem polynomial.nat_degree_mul {R : Type u} [semiring R] {p q : polynomial R} (hp : p 0) (hq : q 0) :
(p * q).nat_degree =
@[simp]
theorem polynomial.nat_degree_pow {R : Type u} [semiring R] (p : polynomial R) (n : ) :
theorem polynomial.degree_le_mul_left {R : Type u} [semiring R] {q : polynomial R} (p : polynomial R) (hq : q 0) :
p.degree (p * q).degree
theorem polynomial.nat_degree_le_of_dvd {R : Type u} [semiring R] {p q : polynomial R} (h1 : p q) (h2 : q 0) :
theorem polynomial.degree_le_of_dvd {R : Type u} [semiring R] {p q : polynomial R} (h1 : p q) (h2 : q 0) :
theorem polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h₁ : p q) (h₂ : q.degree < p.degree) :
q = 0
theorem polynomial.eq_zero_of_dvd_of_nat_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h₁ : p q) (h₂ : q.nat_degree < p.nat_degree) :
q = 0
theorem polynomial.not_dvd_of_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h0 : q 0) (hl : q.degree < p.degree) :
¬p q
theorem polynomial.not_dvd_of_nat_degree_lt {R : Type u} [semiring R] {p q : polynomial R} (h0 : q 0) (hl : q.nat_degree < p.nat_degree) :
¬p q
theorem polynomial.nat_degree_sub_eq_of_prod_eq {R : Type u} [semiring 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₁) :

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

@[simp]
theorem polynomial.degree_coe_units {R : Type u} [semiring R] [nontrivial R] (u : (polynomial R)ˣ) :
theorem polynomial.is_unit_iff {R : Type u} [semiring R] {p : polynomial R} :
(r : R),
@[simp]
theorem polynomial.degree_bit0_eq {R : Type u} [semiring R] [char_zero R] (p : polynomial R) :
theorem polynomial.degree_bit1_eq {R : Type u} [semiring R] [char_zero R] {p : polynomial R} (hp : 0 < p.degree) :
theorem polynomial.irreducible_of_monic {R : Type u} {p : polynomial R} (hp : p.monic) (hp1 : p 1) :
(f g : , f.monic g.monic f * g = p f = 1 g = 1
theorem polynomial.monic.irreducible_iff_nat_degree {R : Type u} {p : polynomial R} (hp : p.monic) :
p 1 (f g : , f.monic g.monic f * g = p f.nat_degree = 0 g.nat_degree = 0
theorem polynomial.monic.irreducible_iff_nat_degree' {R : Type u} {p : polynomial R} (hp : p.monic) :
p 1 (f g : , f.monic g.monic f * g = p g.nat_degree (p.nat_degree / 2)
theorem polynomial.monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} {p : polynomial R} (hm : p.monic) (hnd : p.nat_degree = 2) :
(c₁ c₂ : R), p.coeff 0 = c₁ * c₂ p.coeff 1 = c₁ + c₂
theorem polynomial.root_mul {R : Type u} {a : R} {p q : polynomial R} :
(p * q).is_root a p.is_root a q.is_root a
theorem polynomial.root_or_root_of_root_mul {R : Type u} {a : R} {p q : polynomial R} (h : (p * q).is_root a) :
@[protected, instance]
def polynomial.is_domain {R : Type u} [ring R] [is_domain R] :
theorem polynomial.le_root_multiplicity_iff {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p 0) {a : R} {n : } :
^ n p

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

theorem polynomial.root_multiplicity_le_iff {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p 0) (a : R) (n : ) :
¬ ^ (n + 1) p
theorem polynomial.pow_root_multiplicity_not_dvd {R : Type u} [comm_ring R] {p : polynomial R} (p0 : p 0) (a : R) :
¬ ^ p
theorem polynomial.root_multiplicity_add {R : Type u} [comm_ring R] {p q : polynomial R} (a : R) (hzero : p + q 0) :

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

theorem polynomial.prime_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
theorem polynomial.prime_X {R : Type u} [comm_ring R] [is_domain R] :
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) :
theorem polynomial.irreducible_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
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) :
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 : q) :
p = q
theorem polynomial.root_multiplicity_mul {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} {x : R} (hpq : p * q 0) :
theorem polynomial.root_multiplicity_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {x y : R} :
= ite (x = y) 1 0
theorem polynomial.root_multiplicity_X_sub_C_pow {R : Type u} [comm_ring R] [is_domain R] (a : R) (n : ) :
= n

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

theorem polynomial.exists_multiset_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p 0) :
(s : multiset R), p.degree (a : R),
noncomputable def polynomial.roots {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :

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

Equations
@[simp]
theorem polynomial.roots_zero {R : Type u} [comm_ring R] [is_domain R] :
0.roots = 0
theorem polynomial.card_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp0 : p 0) :
theorem polynomial.card_roots' {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
theorem polynomial.card_roots_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a : R} (hp0 : 0 < p.degree) :
theorem polynomial.card_roots_sub_C' {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a : R} (hp0 : 0 < p.degree) :
@[simp]
theorem polynomial.count_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] (p : polynomial R) :
@[simp]
theorem polynomial.mem_roots' {R : Type u} {a : R} [comm_ring R] [is_domain R] {p : polynomial R} :
a p.roots p 0 p.is_root a
theorem polynomial.mem_roots {R : Type u} {a : R} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p 0) :
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
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) :
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
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
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₀
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
theorem polynomial.eq_of_infinite_eval_eq {R : Type u} [comm_ring R] [is_domain R] (p q : polynomial R) (h : {x : R | = q}.infinite) :
p = q
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
theorem polynomial.roots.le_of_dvd {R : Type u} [comm_ring R] [is_domain R] {p q : polynomial R} (h : q 0) :
theorem polynomial.mem_roots_sub_C' {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} {a x : R} :
x (p - .roots = a
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 - .roots = a
@[simp]
theorem polynomial.roots_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (r : R) :
= {r}
@[simp]
theorem polynomial.roots_X {R : Type u} [comm_ring R] [is_domain R] :
@[simp]
theorem polynomial.roots_C {R : Type u} [comm_ring R] [is_domain R] (x : R) :
.roots = 0
@[simp]
theorem polynomial.roots_one {R : Type u} [comm_ring R] [is_domain R] :
@[simp]
theorem polynomial.roots_C_mul {R : Type u} {a : R} [comm_ring R] [is_domain R] (p : polynomial R) (ha : a 0) :
* p).roots = p.roots
@[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
theorem polynomial.roots_list_prod {R : Type u} [comm_ring R] [is_domain R] (L : list (polynomial R)) :
0 L
theorem polynomial.roots_prod {R : Type u} [comm_ring R] [is_domain R] {ι : Type u_1} (f : ι ) (s : finset ι) :
s.prod f 0 (s.prod f).roots = s.val.bind (λ (i : ι), (f i).roots)
@[simp]
theorem polynomial.roots_pow {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) (n : ) :
(p ^ n).roots = n p.roots
theorem polynomial.roots_X_pow {R : Type u} [comm_ring R] [is_domain R] (n : ) :
.roots = n {0}
theorem polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [comm_ring R] [is_domain R] (ha : a 0) (n : ) :
* .roots = n {0}
@[simp]
theorem polynomial.roots_monomial {R : Type u} {a : R} [comm_ring R] [is_domain R] (ha : a 0) (n : ) :
( a).roots = n {0}
theorem polynomial.roots_prod_X_sub_C {R : Type u} [comm_ring R] [is_domain R] (s : finset R) :
(s.prod (λ (a : R), .roots = s.val
@[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), s).prod.roots = s
theorem polynomial.card_roots_X_pow_sub_C {R : Type u} [comm_ring R] [is_domain R] {n : } (hn : 0 < n) (a : R) :
n
noncomputable def polynomial.nth_roots {R : Type u} [comm_ring R] [is_domain R] (n : ) (a : R) :

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

Equations
@[simp]
theorem polynomial.mem_nth_roots {R : Type u} [comm_ring R] [is_domain R] {n : } (hn : 0 < n) {a x : R} :
x ^ n = a
@[simp]
theorem polynomial.nth_roots_zero {R : Type u} [comm_ring R] [is_domain R] (r : R) :
theorem polynomial.card_nth_roots {R : Type u} [comm_ring R] [is_domain R] (n : ) (a : R) :
@[simp]
theorem polynomial.nth_roots_two_eq_zero_iff {R : Type u} [comm_ring R] [is_domain R] {r : R} :
noncomputable def polynomial.nth_roots_finset (n : ) (R : Type u_1) [comm_ring R] [is_domain R] :

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

Equations
@[simp]
theorem polynomial.mem_nth_roots_finset {R : Type u} [comm_ring R] [is_domain R] {n : } (h : 0 < n) {x : R} :
x ^ n = 1
@[simp]
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
theorem polynomial.monic.comp_X_add_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) (r : R) :
theorem polynomial.monic.comp_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) (r : R) :
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
@[simp]
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)
theorem polynomial.zero_of_eval_zero {R : Type u} [comm_ring R] [is_domain R] [infinite R] (p : polynomial R) (h : (x : R), = 0) :
p = 0
theorem polynomial.funext {R : Type u} [comm_ring R] [is_domain R] [infinite R] {p q : polynomial R} (ext : (r : R), = ) :
p = q
def polynomial.root_set {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [ 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`
theorem polynomial.root_set_def {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [ S] :
@[simp]
theorem polynomial.root_set_C {S : Type v} {T : Type w} [comm_ring T] [comm_ring S] [is_domain S] [ S] (a : T) :
S =
@[simp]
theorem polynomial.root_set_zero {T : Type w} [comm_ring T] (S : Type u_1) [comm_ring S] [is_domain S] [ S] :
@[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] [ S] :
Equations
theorem polynomial.root_set_finite {T : Type w} [comm_ring T] (p : polynomial T) (S : Type u_1) [comm_ring S] [is_domain S] [ S] :
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 : (hf : f.nat_degree d (i : ), f.coeff i U), f).roots.to_finset)).finite

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

theorem polynomial.mem_root_set' {T : Type w} [comm_ring T] {p : polynomial T} {S : Type u_1} [comm_ring S] [is_domain S] [ S] {a : S} :
a p.root_set S p 0 p = 0
theorem polynomial.mem_root_set {T : Type w} [comm_ring T] {p : polynomial T} {S : Type u_1} [comm_ring S] [is_domain S] [ S] {a : S} :
a p.root_set S p 0 p = 0
theorem polynomial.mem_root_set_of_ne {T : Type w} [comm_ring T] {p : polynomial T} {S : Type u_1} [comm_ring S] [is_domain S] [ S] (hp : p 0) {a : S} :
a p.root_set S p = 0
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] [ S] [comm_ring S'] [is_domain S'] [ S'] (hp : polynomial.map S') p = 0 p = 0) (f : S →ₐ[T] S') :
(p.root_set S) (p.root_set S')
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] [ S] {a : S} (h : a p.root_set S) :
p 0
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] [ S] {a : S} (hx : a p.root_set S) :
p = 0
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] [ S] [comm_ring S'] [is_domain S'] [ S'] [ S'] (f : S →ₐ[T] S') :
(p.root_set S) (p.root_set S')
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
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) :

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

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 =
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
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)) :
theorem polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [field K] {I : Type v} {s : I K} (H : function.injective s) :
theorem polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
(multiset.map (λ (a : R), p.roots).prod p

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

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), s).prod p s p.roots

A Galois connection.

theorem polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
(q : , (multiset.map (λ (a : R), p.roots).prod * q = p q.roots = 0
theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hroots : = p.nat_degree) :
* (multiset.map (λ (a : R), 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`.

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 : = p.nat_degree) :
(multiset.map (λ (a : R), 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`.

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 : 0) (a : A) :
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) :
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 : 0) (b : B) :
p.roots)
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) :
p.roots)
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 : 0) :
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) :
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 : 0) :
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) :
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 : = p.nat_degree) :
= p).roots
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 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`.