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} :
p 0¬is_unit p0 < p.degree

theorem polynomial.irreducible_of_monic {R : Type u} [field R] {p : polynomial R} :
p.monicp 1(irreducible p ∀ (f g : polynomial R), f.monicg.monicf * g = pf = 1 g = 1)

def polynomial.div {R : Type u} [field R] :

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

Equations
def polynomial.mod {R : Type u} [field 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) :
q.monicp %ₘ q = p % q

theorem polynomial.div_by_monic_eq_div {R : Type u} [field R] {q : polynomial R} (p : polynomial R) :
q.monicp /ₘ q = p / q

theorem polynomial.mod_eq_self_iff {R : Type u} [field R] {p q : polynomial R} :
q 0(p % q = p p.degree < q.degree)

theorem polynomial.div_eq_zero_iff {R : Type u} [field R] {p q : polynomial R} :
q 0(p / q = 0 p.degree < q.degree)

theorem polynomial.degree_add_div {R : Type u} [field R] {p q : polynomial R} :
q 0q.degree p.degreeq.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} :
p 00 < 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} :

theorem polynomial.eval_gcd_eq_zero {R : Type u} [field R] {f g : polynomial R} {α : R} :

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} :

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} :

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} :
p 0polynomial.map f 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} :
p 0(x (polynomial.map f p).roots polynomial.eval₂ f x p = 0)

theorem polynomial.exists_root_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} :
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} :
p 0(normalize p).monic

theorem polynomial.normalize_monic {R : Type u} [field R] {p : polynomial R} :
p.monicnormalize p = p

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} :
p.degree = 1prime p

theorem polynomial.irreducible_of_degree_eq_one {R : Type u} [field R] {p : polynomial R} :
p.degree = 1irreducible p

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} :
irreducible p0 < p.degree

theorem polynomial.pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v} {s : I → α} :

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} :
p 0(multiset.map (λ (a : R), polynomial.X - polynomial.C a) p.roots).prod = ∏ (a : R) in p.roots.to_finset, (λ (a : R), (polynomial.X - polynomial.C a) ^ polynomial.root_multiplicity a p) a

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} :
a 0((polynomial.C a) * p).roots = p.roots