# mathlibdocumentation

data.polynomial.ring_division

# Theory of univariate polynomials

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

theorem polynomial.nat_degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {p : polynomial R} (hp : p 0) {z : S} :
p = 0(∀ (x : R), S) x = 0x = 0)0 < p.nat_degree

theorem polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {p : polynomial R} (hp : p 0) {z : S} :
p = 0(∀ (x : R), S) x = 0x = 0)0 < p.degree

@[instance]
def polynomial.integral_domain {R : Type u}  :

Equations
theorem polynomial.nat_degree_mul {R : Type u} {p q : polynomial R} :
p 0q 0(p * q).nat_degree =

@[simp]
theorem polynomial.nat_degree_pow {R : Type u} (p : polynomial R) (n : ) :

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} :
(p * q).is_root ap.is_root a q.is_root a

theorem polynomial.degree_le_mul_left {R : Type u} {q : polynomial R} (p : polynomial R) :
q 0p.degree (p * q).degree

theorem polynomial.nat_degree_le_of_dvd {R : Type u} {p q : polynomial R} :
p qq 0

theorem polynomial.degree_eq_zero_of_is_unit {R : Type u} {p : polynomial R} :
p.degree = 0

@[simp]
theorem polynomial.degree_coe_units {R : Type u} (u : units (polynomial R)) :

theorem polynomial.prime_X_sub_C {R : Type u} {r : R} :

theorem polynomial.prime_X {R : Type u}  :

theorem polynomial.prime_of_degree_eq_one_of_monic {R : Type u} {p : polynomial R} :
p.degree = 1p.monic

theorem polynomial.irreducible_X_sub_C {R : Type u} (r : R) :

theorem polynomial.irreducible_X {R : Type u}  :

theorem polynomial.irreducible_of_degree_eq_one_of_monic {R : Type u} {p : polynomial R} :
p.degree = 1p.monic

theorem polynomial.eq_of_monic_of_associated {R : Type u} {p q : polynomial R} :
p.monicq.monic qp = q

@[simp]
theorem polynomial.root_multiplicity_zero {R : Type u} {x : R} :

theorem polynomial.root_multiplicity_eq_zero {R : Type u} {p : polynomial R} {x : R} :
¬p.is_root x

theorem polynomial.root_multiplicity_pos {R : Type u} {p : polynomial R} (hp : p 0) {x : R} :

theorem polynomial.root_multiplicity_mul {R : Type u} {p q : polynomial R} {x : R} :
p * q 0

theorem polynomial.root_multiplicity_X_sub_C_self {R : Type u} {x : R} :

theorem polynomial.root_multiplicity_X_sub_C {R : Type u} {x y : R} :
= ite (x = y) 1 0

theorem polynomial.root_multiplicity_X_sub_C_pow {R : Type u} (a : R) (n : ) :
= n

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

theorem polynomial.root_multiplicity_of_dvd {R : Type u} {p : polynomial R} {a : R} {n : } :
p 0 ^ n p

If (X - a) ^ n divides a polynomial p then the multiplicity of a as root of p is at least n.

theorem polynomial.root_multiplicity_add {R : Type u} {p q : polynomial R} (a : R) :
p + q 0 (p + q)

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

theorem polynomial.exists_multiset_roots {R : Type u} {p : polynomial R} :
p 0(∃ (s : multiset R), (s.card) p.degree ∀ (a : R),

def polynomial.roots {R : Type u}  :

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

Equations
@[simp]
theorem polynomial.roots_zero {R : Type u}  :
0.roots = 0

theorem polynomial.card_roots {R : Type u} {p : polynomial R} :
p 0(p.roots.card) p.degree

theorem polynomial.card_roots' {R : Type u} {p : polynomial R} :

theorem polynomial.card_roots_sub_C {R : Type u} {p : polynomial R} {a : R} :
0 < p.degree((p - .roots.card) p.degree

theorem polynomial.card_roots_sub_C' {R : Type u} {p : polynomial R} {a : R} :
0 < p.degree(p - .roots.card p.nat_degree

@[simp]
theorem polynomial.count_roots {R : Type u} {a : R} {p : polynomial R} :
p 0

@[simp]
theorem polynomial.mem_roots {R : Type u} {a : R} {p : polynomial R} :
p 0(a p.roots p.is_root a)

theorem polynomial.eq_zero_of_infinite_is_root {R : Type u} (p : polynomial R) :
{x : R | p.is_root x}.infinitep = 0

theorem polynomial.eq_of_infinite_eval_eq {R : Type u_1} (p q : polynomial R) :
{x : R | = q}.infinitep = q

theorem polynomial.roots_mul {R : Type u} {p q : polynomial R} :
p * q 0(p * q).roots = p.roots + q.roots

@[simp]
theorem polynomial.mem_roots_sub_C {R : Type u} {p : polynomial R} {a x : R} :
0 < p.degree(x (p - .roots = a)

@[simp]
theorem polynomial.roots_X_sub_C {R : Type u} (r : R) :
= r ::ₘ 0

@[simp]
theorem polynomial.roots_C {R : Type u} (x : R) :
.roots = 0

@[simp]
theorem polynomial.roots_one {R : Type u}  :

theorem polynomial.roots_list_prod {R : Type u} (L : list (polynomial R)) :
(∀ (p : , p Lp 0)

theorem polynomial.roots_multiset_prod {R : Type u} (m : multiset (polynomial R)) :
(∀ (p : , p mp 0)

theorem polynomial.roots_prod {R : Type u} {ι : Type u_1} (f : ι → ) (s : finset ι) :
s.prod f 0(s.prod f).roots = s.val.bind (λ (i : ι), (f i).roots)

theorem polynomial.roots_prod_X_sub_C {R : Type u} (s : finset R) :
(∏ (a : R) in s, .roots = s.val

theorem polynomial.card_roots_X_pow_sub_C {R : Type u} {n : } (hn : 0 < n) (a : R) :

def polynomial.nth_roots {R : Type u}  :
R →

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

Equations
@[simp]
theorem polynomial.mem_nth_roots {R : Type u} {n : } (hn : 0 < n) {a x : R} :
x ^ n = a

@[simp]
theorem polynomial.nth_roots_zero {R : Type u} (r : R) :

theorem polynomial.card_nth_roots {R : Type u} (n : ) (a : R) :
a).card n

def polynomial.nth_roots_finset (n : ℕ+) (R : Type u_1)  :

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

Equations
@[simp]
theorem polynomial.mem_nth_roots_finset {R : Type u} {n : ℕ+} {x : R} :
x ^ n = 1

theorem polynomial.nat_degree_comp {R : Type u} {p q : polynomial R} :

theorem polynomial.leading_coeff_comp {R : Type u} {p q : polynomial R} :

theorem polynomial.units_coeff_zero_smul {R : Type u} (c : units (polynomial R)) (p : polynomial R) :
c.coeff 0 p = (c) * p

@[simp]
theorem polynomial.nat_degree_coe_units {R : Type u} (u : units (polynomial R)) :

theorem polynomial.zero_of_eval_zero {R : Type u} [infinite R] (p : polynomial R) :
(∀ (x : R), = 0)p = 0

theorem polynomial.funext {R : Type u} [infinite R] {p q : polynomial R} :
(∀ (r : R), = q)p = q

theorem polynomial.is_unit_iff {R : Type u} {f : polynomial R} :
∃ (r : R),

theorem polynomial.degree_eq_degree_of_associated {R : Type u} {p q : polynomial R} :
qp.degree = q.degree

theorem polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} {p : polynomial R} (hi : irreducible p) {x : R} :
p.is_root xp.degree = 1

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

theorem polynomial.is_unit_of_is_unit_leading_coeff_of_is_unit_map {R : Type u} {S : Type v} [semiring R] (φ : R →+* S) (f : polynomial R) :
is_unit f)

theorem polynomial.irreducible_of_irreducible_map {R : Type u} {S : Type v} (φ : R →+* S) (f : polynomial R) :
f.monic

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.

theorem is_integral_domain.polynomial {R : Type u_1} [comm_ring R] :

Lift evidence that is_integral_domain R to is_integral_domain (polynomial R).