mathlib3 documentation

data.polynomial.field_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] $

theorem polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [division_ring R] {p : polynomial R} (hp0 : p 0) (hp : ¬is_unit p) :
0 < p.degree
@[simp]
theorem polynomial.map_eq_zero {R : Type u} {S : Type v} [division_ring R] {p : polynomial R} [semiring S] [nontrivial S] (f : R →+* S) :
polynomial.map f p = 0 p = 0
theorem polynomial.map_ne_zero {R : Type u} {S : Type v} [division_ring R] {p : polynomial R} [semiring S] [nontrivial S] {f : R →+* S} (hp : p 0) :
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.mod_def {R : Type u} [field R] {p q : polynomial R} :
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_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] [division_ring k] (p : polynomial R) (f : R →+* k) :
@[simp]
theorem polynomial.nat_degree_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [division_ring k] (f : R →+* k) :
@[simp]
theorem polynomial.monic_map_iff {R : Type u} {k : Type y} [field R] [division_ring k] {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) :
theorem polynomial.map_mod {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
theorem polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hf : polynomial.eval₂ ϕ α f = 0) (hg : polynomial.eval₂ ϕ α g = 0) :
theorem polynomial.eval_gcd_eq_zero {R : Type u} [field R] {f g : polynomial R} {α : R} (hf : polynomial.eval α f = 0) (hg : polynomial.eval α g = 0) :
theorem polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :
theorem polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : polynomial R} {α : k} (hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :
theorem polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [field R] [comm_semiring k] {ϕ : R →+* k} {f g : polynomial R} {α : k} :
theorem polynomial.is_coprime_map {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
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) :
theorem polynomial.root_set_monomial {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [algebra R S] {n : } (hn : n 0) {a : R} (ha : a 0) :
theorem polynomial.root_set_C_mul_X_pow {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [algebra R S] {n : } (hn : n 0) {a : R} (ha : a 0) :
theorem polynomial.root_set_X_pow {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [algebra R S] {n : } (hn : n 0) :
theorem polynomial.root_set_prod {R : Type u} {S : Type v} [field R] [comm_ring S] [is_domain S] [algebra R S] {ι : Type u_1} (f : ι polynomial R) (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.div_C_mul {R : Type u} {a : R} [field R] {p q : polynomial R} :
theorem polynomial.C_mul_dvd {R : Type u} {a : R} [field R] {p q : polynomial R} (ha : a 0) :
theorem polynomial.dvd_C_mul {R : Type u} {a : R} [field R] {p q : polynomial R} (ha : a 0) :
theorem polynomial.normalize_monic {R : Type u} [field R] {p : polynomial R} (h : p.monic) :
theorem polynomial.map_dvd_map' {R : Type u} {k : Type y} [field R] [field k] (f : R →+* k) {x y : polynomial R} :
theorem polynomial.prime_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} (hp1 : p.degree = 1) :
theorem polynomial.degree_pos_of_irreducible {R : Type u} [field R] {p : polynomial R} (hp : irreducible p) :
0 < p.degree

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).