# mathlibdocumentation

data.polynomial.field_division

# Theory of univariate polynomials #

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

theorem polynomial.roots_C_mul {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) {a : R} (hzero : a 0) :
* p).roots = p.roots
theorem polynomial.derivative_root_multiplicity_of_root {R : Type u} [comm_ring R] [is_domain R] [char_zero R] {p : polynomial R} {t : R} (hpt : p.is_root t) :
@[protected, instance]
noncomputable def polynomial.normalization_monoid {R : Type u} [comm_ring R] [is_domain R]  :
Equations
@[simp]
theorem polynomial.coe_norm_unit {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} :
theorem polynomial.leading_coeff_normalize {R : Type u} [comm_ring R] [is_domain R] (p : polynomial R) :
theorem polynomial.monic.normalize_eq_self {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p.monic) :
= p
theorem polynomial.roots_normalize {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} :
theorem polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} {p : polynomial R} (hp0 : p 0) (hp : ¬) :
0 < p.degree
theorem polynomial.monic_mul_leading_coeff_inv {R : Type u} {p : polynomial R} (h : p 0) :
(p * .monic
theorem polynomial.degree_mul_leading_coeff_inv {R : Type u} {q : polynomial R} (p : polynomial R) (h : q 0) :
@[simp]
theorem polynomial.map_eq_zero {R : Type u} {S : Type v} {p : polynomial R} [semiring S] [nontrivial S] (f : R →+* S) :
= 0 p = 0
theorem polynomial.map_ne_zero {R : Type u} {S : Type v} {p : polynomial R} [semiring S] [nontrivial S] {f : R →+* S} (hp : p 0) :
0
theorem polynomial.is_unit_iff_degree_eq_zero {R : Type u} [field R] {p : polynomial R} :
p.degree = 0
theorem polynomial.irreducible_of_monic {R : Type u} [field R] {p : polynomial R} (hp1 : p.monic) (hp2 : p 1) :
∀ (f g : , f.monicg.monicf * g = pf = 1 g = 1
noncomputable def polynomial.div {R : Type u} [field R] (p q : polynomial R) :

Division of polynomials. See polynomial.div_by_monic for more details.

Equations
noncomputable def polynomial.mod {R : Type u} [field R] (p q : polynomial R) :

Remainder of polynomial division. See polynomial.mod_by_monic for more details.

Equations
@[protected, instance]
noncomputable def polynomial.has_div {R : Type u} [field R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_mod {R : Type u} [field R] :
Equations
theorem polynomial.div_def {R : Type u} [field R] {p q : polynomial R} :
p / q = * (p /ₘ (q *
theorem polynomial.mod_def {R : Type u} [field R] {p q : polynomial R} :
p % q = p %ₘ (q *
theorem polynomial.mod_by_monic_eq_mod {R : Type u} [field R] {q : polynomial R} (p : polynomial R) (hq : q.monic) :
p %ₘ q = p % q
theorem polynomial.div_by_monic_eq_div {R : Type u} [field R] {q : polynomial R} (p : polynomial R) (hq : q.monic) :
p /ₘ q = p / q
theorem polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [field R] (p : polynomial R) (a : R) :
p % =
theorem polynomial.mul_div_eq_iff_is_root {R : Type u} {a : R} [field R] {p : polynomial R} :
* (p / = p p.is_root a
@[protected, instance]
noncomputable def polynomial.euclidean_domain {R : Type u} [field R] :
Equations
theorem polynomial.mod_eq_self_iff {R : Type u} [field R] {p q : polynomial R} (hq0 : q 0) :
p % q = p p.degree < q.degree
theorem polynomial.div_eq_zero_iff {R : Type u} [field R] {p q : polynomial R} (hq0 : q 0) :
p / q = 0 p.degree < q.degree
theorem polynomial.degree_add_div {R : Type u} [field R] {p q : polynomial R} (hq0 : q 0) (hpq : q.degree p.degree) :
q.degree + (p / q).degree = p.degree
theorem polynomial.degree_div_le {R : Type u} [field R] (p q : polynomial R) :
(p / q).degree p.degree
theorem polynomial.degree_div_lt {R : Type u} [field R] {p q : polynomial R} (hp : p 0) (hq : 0 < q.degree) :
(p / q).degree < p.degree
@[simp]
theorem polynomial.degree_map {R : Type u} {k : Type y} [field R] (p : polynomial R) (f : R →+* k) :
@[simp]
theorem polynomial.nat_degree_map {R : Type u} {k : Type y} [field R] {p : polynomial R} (f : R →+* k) :
@[simp]
theorem polynomial.leading_coeff_map {R : Type u} {k : Type y} [field R] {p : polynomial R} (f : R →+* k) :
theorem polynomial.monic_map_iff {R : Type u} {k : Type y} [field R] {f : R →+* k} {p : polynomial R} :
theorem polynomial.is_unit_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [field k] (f : R →+* k) :
theorem polynomial.map_div {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
(p / q) = /
theorem polynomial.map_mod {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
(p % q) = %
theorem polynomial.gcd_map {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
q) =
theorem polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [field R] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hf : f = 0) (hg : g = 0) :
g) = 0
theorem polynomial.eval_gcd_eq_zero {R : Type u} [field R] {f g : polynomial R} {α : R} (hf : = 0) (hg : = 0) :
= 0
theorem polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [field R] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hα : g) = 0) :
f = 0
theorem polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [field R] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hα : g) = 0) :
g = 0
theorem polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [field R] {ϕ : R →+* k} {f g : polynomial R} {α : k} :
g) = 0 f = 0 g = 0
theorem polynomial.is_root_gcd_iff_is_root_left_right {R : Type u} [field R] {f g : polynomial R} {α : R} :
g).is_root α f.is_root α g.is_root α
theorem polynomial.is_coprime_map {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
is_coprime p) q) q
theorem polynomial.mem_roots_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [comm_ring k] [is_domain k] {f : R →+* k} {x : k} (hp : p 0) :
x p).roots p = 0
theorem polynomial.mem_root_set {R : Type u} {k : Type y} [field R] {p : polynomial R} [comm_ring k] [is_domain k] [ k] {x : k} (hp : p 0) :
x p.root_set k p = 0
theorem polynomial.root_set_C_mul_X_pow {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [ S] {n : } (hn : n 0) {a : R} (ha : a 0) :
* .root_set S = {0}
theorem polynomial.root_set_monomial {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [ S] {n : } (hn : n 0) {a : R} (ha : a 0) :
( a).root_set S = {0}
theorem polynomial.root_set_X_pow {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [ S] {n : } (hn : n 0) :
.root_set S = {0}
theorem polynomial.root_set_prod {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [ S] {ι : Type u_1} (f : ι → ) (s : finset ι) (h : s.prod f 0) :
(s.prod f).root_set S = ⋃ (i : ι) (H : i s), (f i).root_set S
theorem polynomial.exists_root_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} (h : p.degree = 1) :
∃ (x : R), p.is_root x
theorem polynomial.coeff_inv_units {R : Type u} [field R] (u : (polynomial R)ˣ) (n : ) :
theorem polynomial.monic_normalize {R : Type u} [field R] {p : polynomial R} (hp0 : p 0) :
theorem polynomial.leading_coeff_div {R : Type u} [field R] {p q : polynomial R} (hpq : q.degree p.degree) :
theorem polynomial.div_C_mul {R : Type u} {a : R} [field R] {p q : polynomial R} :
p / * q) = * (p / q)
theorem polynomial.C_mul_dvd {R : Type u} {a : R} [field R] {p q : polynomial R} (ha : a 0) :
q p q
theorem polynomial.dvd_C_mul {R : Type u} {a : R} [field R] {p q : polynomial R} (ha : a 0) :
p p q
theorem polynomial.coe_norm_unit_of_ne_zero {R : Type u} [field R] {p : polynomial R} (hp : p 0) :
theorem polynomial.normalize_monic {R : Type u} [field R] {p : polynomial R} (h : p.monic) :
= p
theorem polynomial.map_dvd_map' {R : Type u} {k : Type y} [field R] [field k] (f : R →+* k) {x y : polynomial R} :
x y
theorem polynomial.degree_normalize {R : Type u} [field R] {p : polynomial R} :
theorem polynomial.prime_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} (hp1 : p.degree = 1) :
theorem polynomial.irreducible_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} (hp1 : p.degree = 1) :
theorem polynomial.not_irreducible_C {R : Type u} [field R] (x : R) :
theorem polynomial.degree_pos_of_irreducible {R : Type u} [field R] {p : polynomial R} (hp : irreducible p) :
0 < p.degree
theorem polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero {K : Type u_1} [field K] (f : polynomial K) (a : K) (hf' : 0) :
(f /ₘ

If f is a polynomial over a field, and a : K satisfies f' a ≠ 0, then f / (X - a) is coprime with X - a. Note that we do not assume f a = 0, because f / (X - a) = (f - f a) / (X - a).