mathlib documentation

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] [algebra R S] {p : polynomial R} (hp : p 0) {z : S} (hz : (polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebra_map R S) x = 0x = 0) :
theorem polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {p : polynomial R} (hp : p 0) {z : S} (hz : (polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebra_map R S) x = 0x = 0) :
0 < p.degree
theorem polynomial.aeval_mod_by_monic_eq_self_of_root {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {p q : polynomial R} (hq : q.monic) {x : S} (hx : (polynomial.aeval x) q = 0) :
theorem polynomial.nat_degree_mul {R : Type u} [comm_ring R] [no_zero_divisors R] {p q : polynomial R} (hp : p 0) (hq : q 0) :
@[simp]
theorem polynomial.nat_degree_pow {R : Type u} [comm_ring R] [no_zero_divisors R] (p : polynomial R) (n : ) :
theorem polynomial.root_mul {R : Type u} {a : R} [comm_ring R] [no_zero_divisors 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} [comm_ring R] [no_zero_divisors R] {p q : polynomial R} (h : (p * q).is_root a) :
theorem polynomial.degree_le_mul_left {R : Type u} [comm_ring R] [no_zero_divisors R] {q : polynomial R} (p : polynomial R) (hq : q 0) :
p.degree (p * q).degree
theorem polynomial.nat_degree_le_of_dvd {R : Type u} [comm_ring R] [no_zero_divisors R] {p q : polynomial R} (h1 : p q) (h2 : q 0) :
theorem polynomial.degree_eq_zero_of_is_unit {R : Type u} [integral_domain R] {p : polynomial R} (h : is_unit p) :
p.degree = 0
@[simp]
theorem polynomial.degree_coe_units {R : Type u} [integral_domain R] (u : units (polynomial R)) :
theorem polynomial.prime_of_degree_eq_one_of_monic {R : Type u} [integral_domain R] {p : polynomial R} (hp1 : p.degree = 1) (hm : p.monic) :
theorem polynomial.irreducible_of_degree_eq_one_of_monic {R : Type u} [integral_domain R] {p : polynomial R} (hp1 : p.degree = 1) (hm : p.monic) :
theorem polynomial.eq_of_monic_of_associated {R : Type u} [integral_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (hpq : associated p q) :
p = q
@[simp]
theorem polynomial.root_multiplicity_pos {R : Type u} [integral_domain R] {p : polynomial R} (hp : p 0) {x : R} :

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

theorem polynomial.root_multiplicity_of_dvd {R : Type u} [integral_domain R] {p : polynomial R} {a : R} {n : } (hzero : p 0) (h : (polynomial.X - polynomial.C a) ^ n p) :

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

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

theorem polynomial.exists_multiset_roots {R : Type u} [integral_domain R] {p : polynomial R} (hp : p 0) :
def polynomial.roots {R : Type u} [integral_domain R] (p : polynomial R) :

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

Equations
@[simp]
theorem polynomial.roots_zero {R : Type u} [integral_domain R] :
0.roots = 0
theorem polynomial.card_roots {R : Type u} [integral_domain R] {p : polynomial R} (hp0 : p 0) :
theorem polynomial.card_roots' {R : Type u} [integral_domain R] {p : polynomial R} (hp0 : p 0) :
theorem polynomial.card_roots_sub_C {R : Type u} [integral_domain R] {p : polynomial R} {a : R} (hp0 : 0 < p.degree) :
@[simp]
theorem polynomial.count_roots {R : Type u} {a : R} [integral_domain R] {p : polynomial R} (hp : p 0) :
@[simp]
theorem polynomial.mem_roots {R : Type u} {a : R} [integral_domain R] {p : polynomial R} (hp : p 0) :
theorem polynomial.eq_zero_of_infinite_is_root {R : Type u} [integral_domain R] (p : polynomial R) (h : {x : R | p.is_root x}.infinite) :
p = 0
theorem polynomial.exists_max_root {R : Type u} [integral_domain R] [linear_order R] (p : polynomial R) (hp : p 0) :
∃ (x₀ : R), ∀ (x : R), p.is_root xx x₀
theorem polynomial.exists_min_root {R : Type u} [integral_domain R] [linear_order R] (p : polynomial R) (hp : p 0) :
∃ (x₀ : R), ∀ (x : R), p.is_root xx₀ x
theorem polynomial.eq_of_infinite_eval_eq {R : Type u_1} [integral_domain R] (p q : polynomial R) (h : {x : R | polynomial.eval x p = polynomial.eval x q}.infinite) :
p = q
theorem polynomial.roots_mul {R : Type u} [integral_domain R] {p q : polynomial R} (hpq : p * q 0) :
(p * q).roots = p.roots + q.roots
@[simp]
theorem polynomial.mem_roots_sub_C {R : Type u} [integral_domain R] {p : polynomial R} {a x : R} (hp0 : 0 < p.degree) :
@[simp]
theorem polynomial.roots_X_sub_C {R : Type u} [integral_domain R] (r : R) :
@[simp]
theorem polynomial.roots_C {R : Type u} [integral_domain R] (x : R) :
@[simp]
theorem polynomial.roots_one {R : Type u} [integral_domain R] :
theorem polynomial.roots_prod {R : Type u} [integral_domain R] {ι : Type u_1} (f : ι → polynomial R) (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} [integral_domain R] (s : finset R) :
(∏ (a : R) in s, (polynomial.X - polynomial.C a)).roots = s.val
theorem polynomial.card_roots_X_pow_sub_C {R : Type u} [integral_domain R] {n : } (hn : 0 < n) (a : R) :
def polynomial.nth_roots {R : Type u} [integral_domain R] (n : ) (a : R) :

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

Equations
@[simp]
theorem polynomial.mem_nth_roots {R : Type u} [integral_domain R] {n : } (hn : 0 < n) {a x : R} :
@[simp]
theorem polynomial.nth_roots_zero {R : Type u} [integral_domain R] (r : R) :
def polynomial.nth_roots_finset (n : ) (R : Type u_1) [integral_domain R] :

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

Equations
@[simp]
theorem polynomial.mem_nth_roots_finset {R : Type u} [integral_domain R] {n : } (h : 0 < n) {x : R} :
theorem polynomial.units_coeff_zero_smul {R : Type u} [integral_domain R] (c : units (polynomial R)) (p : polynomial R) :
c.coeff 0 p = (c) * p
@[simp]
theorem polynomial.comp_eq_zero_iff {R : Type u} [integral_domain R] {p q : polynomial R} :
p.comp q = 0 p = 0 polynomial.eval (q.coeff 0) p = 0 q = polynomial.C (q.coeff 0)
theorem polynomial.zero_of_eval_zero {R : Type u} [integral_domain R] [infinite R] (p : polynomial R) (h : ∀ (x : R), polynomial.eval x p = 0) :
p = 0
theorem polynomial.funext {R : Type u} [integral_domain R] [infinite R] {p q : polynomial R} (ext : ∀ (r : R), polynomial.eval r p = polynomial.eval r q) :
p = q
def polynomial.root_set {R : Type u} [integral_domain R] (p : polynomial R) (S : Type u_1) [integral_domain S] [algebra R S] :
set S

The set of distinct roots of p in E.

If you have a non-separable polynomial, use polynomial.roots for the multiset where multiple roots have the appropriate multiplicity.

Equations
theorem polynomial.root_set_def {R : Type u} [integral_domain R] (p : polynomial R) (S : Type u_1) [integral_domain S] [algebra R S] :
@[simp]
theorem polynomial.root_set_zero {R : Type u} [integral_domain R] (S : Type u_1) [integral_domain S] [algebra R S] :
theorem polynomial.is_unit_iff {R : Type u} [integral_domain R] {f : polynomial R} :
is_unit f ∃ (r : R), is_unit r polynomial.C r = f
theorem polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [integral_domain R] {p : polynomial R} (hi : irreducible p) {x : R} (hx : p.is_root x) :
p.degree = 1
theorem polynomial.leading_coeff_div_by_monic_of_monic {R : Type u} [integral_domain R] {p q : polynomial R} (hmonic : q.monic) (hdegree : q.degree p.degree) :

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

theorem polynomial.eq_of_monic_of_dvd_of_nat_degree_le {R : Type u} [integral_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (hdiv : p q) (hdeg : q.nat_degree p.nat_degree) :
q = p
theorem polynomial.is_unit_of_is_unit_leading_coeff_of_is_unit_map {R : Type u} {S : Type v} [semiring R] [integral_domain S] (φ : R →+* S) (f : polynomial R) (hf : is_unit f.leading_coeff) (H : is_unit (polynomial.map φ f)) :
theorem polynomial.monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [integral_domain R] [integral_domain S] (φ : R →+* S) (f : polynomial R) (h_mon : f.monic) (h_irr : irreducible (polynomial.map φ f)) :

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.