mathlib documentation

data.polynomial.field_division

Theory of univariate polynomials #

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

theorem polynomial.is_unit_iff_degree_eq_zero {R : Type u} [field R] {p : polynomial R} :
theorem polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [field R] {p : polynomial R} (hp0 : p 0) (hp : ¬is_unit p) :
0 < p.degree
theorem polynomial.irreducible_of_monic {R : Type u} [field R] {p : polynomial R} (hp1 : p.monic) (hp2 : p 1) :
irreducible p ∀ (f g : polynomial R), f.monicg.monicf * g = pf = 1 g = 1
def polynomial.div {R : Type u} [field R] (p q : polynomial R) :

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

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

Remainder of polynomial division, see the lemma quotient_mul_add_remainder_eq_aux. See polynomial.mod_by_monic for more details.

Equations
@[instance]
def polynomial.has_div {R : Type u} [field R] :
Equations
@[instance]
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] [field k] (p : polynomial R) (f : R →+* k) :
@[simp]
theorem polynomial.nat_degree_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [field k] (f : R →+* k) :
@[simp]
theorem polynomial.leading_coeff_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [field k] (f : R →+* k) :
theorem polynomial.monic_map_iff {R : Type u} {k : Type y} [field R] [field 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.gcd_map {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_root_gcd_iff_is_root_left_right {R : Type u} [field R] {f g : polynomial R} {α : R} :
theorem polynomial.is_coprime_map {R : Type u} {k : Type y} [field R] {p q : polynomial R} [field k] (f : R →+* k) :
@[simp]
theorem polynomial.map_eq_zero {R : Type u} {S : Type v} [field 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} [field R] {p : polynomial R} [semiring S] [nontrivial S] {f : R →+* S} (hp : p 0) :
theorem polynomial.mem_roots_map {R : Type u} {k : Type y} [field R] {p : polynomial R} [field k] {f : R →+* k} {x : k} (hp : p 0) :
theorem polynomial.mem_root_set {R : Type u} {k : Type y} [field R] {p : polynomial R} [field k] [algebra R k] {x : k} (hp : p 0) :
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 : units (polynomial R)) (n : ) :
theorem polynomial.monic_normalize {R : Type u} [field R] {p : polynomial R} (hp0 : p 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.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.pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v} {s : I → α} (H : function.injective s) :

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

theorem polynomial.prod_multiset_root_eq_finset_root {R : Type u} [field R] {p : polynomial R} (hzero : p 0) :
theorem polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [field R] (p : polynomial R) :

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

theorem polynomial.roots_C_mul {R : Type u} [field R] (p : polynomial R) {a : R} (hzero : a 0) :
theorem polynomial.roots_normalize {R : Type u} [field R] {p : polynomial R} :