mathlib documentation

data.polynomial.ring_division

Theory of univariate polynomials

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

source
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} :
⇑(polynomial.aeval z) p = 0 → (∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) → 0 < p.nat_degree

source
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} :
⇑(polynomial.aeval z) p = 0 → (∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) → 0 < p.degree

source
@[instance]
def polynomial.integral_domain {R : Type u} [integral_domain R] :
integral_domain (polynomial R)

Equations
source
theorem polynomial.nat_degree_mul {R : Type u} [integral_domain R] {p q : polynomial R} :
p ≠ 0 → q ≠ 0 → (p * q).nat_degree = p.nat_degree + q.nat_degree

source
@[simp]
theorem polynomial.nat_degree_pow {R : Type u} [integral_domain R] (p : polynomial R) (n : ℕ) :
(p ^ n).nat_degree = n * p.nat_degree

source
theorem polynomial.root_mul {R : Type u} {a : R} [integral_domain R] {p q : polynomial R} :
(p * q).is_root a ↔ p.is_root a ∨ q.is_root a

source
theorem polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [integral_domain R] {p q : polynomial R} :
(p * q).is_root a → p.is_root a ∨ q.is_root a

source
theorem polynomial.degree_le_mul_left {R : Type u} [integral_domain R] {q : polynomial R} (p : polynomial R) :
q ≠ 0 → p.degree ≤ (p * q).degree

source
theorem polynomial.nat_degree_le_of_dvd {R : Type u} [integral_domain R] {p q : polynomial R} :
p ∣ q → q ≠ 0 → p.nat_degree ≤ q.nat_degree

source
theorem polynomial.degree_eq_zero_of_is_unit {R : Type u} [integral_domain R] {p : polynomial R} :
is_unit p → p.degree = 0

source
@[simp]
theorem polynomial.degree_coe_units {R : Type u} [integral_domain R] (u : units (polynomial R)) :
↑u.degree = 0

source
theorem polynomial.prime_X_sub_C {R : Type u} [integral_domain R] {r : R} :
prime (polynomial.X - ⇑polynomial.C r)

source
theorem polynomial.prime_X {R : Type u} [integral_domain R] :
prime polynomial.X

source
theorem polynomial.prime_of_degree_eq_one_of_monic {R : Type u} [integral_domain R] {p : polynomial R} :
p.degree = 1 → p.monic → prime p

source
theorem polynomial.irreducible_X_sub_C {R : Type u} [integral_domain R] (r : R) :
irreducible (polynomial.X - ⇑polynomial.C r)

source
theorem polynomial.irreducible_X {R : Type u} [integral_domain R] :
irreducible polynomial.X

source
theorem polynomial.irreducible_of_degree_eq_one_of_monic {R : Type u} [integral_domain R] {p : polynomial R} :
p.degree = 1 → p.monic → irreducible p

source
theorem polynomial.eq_of_monic_of_associated {R : Type u} [integral_domain R] {p q : polynomial R} :
p.monic → q.monic → associated p q → p = q

source
@[simp]
theorem polynomial.root_multiplicity_zero {R : Type u} [integral_domain R] {x : R} :
polynomial.root_multiplicity x 0 = 0

source
theorem polynomial.root_multiplicity_eq_zero {R : Type u} [integral_domain R] {p : polynomial R} {x : R} :
¬p.is_root x → polynomial.root_multiplicity x p = 0

source
theorem polynomial.root_multiplicity_pos {R : Type u} [integral_domain R] {p : polynomial R} (hp : p ≠ 0) {x : R} :
0 < polynomial.root_multiplicity x p ↔ p.is_root x

source
theorem polynomial.root_multiplicity_mul {R : Type u} [integral_domain R] {p q : polynomial R} {x : R} :
p * q ≠ 0 → polynomial.root_multiplicity x (p * q) = polynomial.root_multiplicity x p + polynomial.root_multiplicity x q

source
theorem polynomial.root_multiplicity_X_sub_C_self {R : Type u} [integral_domain R] {x : R} :
polynomial.root_multiplicity x (polynomial.X - ⇑polynomial.C x) = 1

source
theorem polynomial.root_multiplicity_X_sub_C {R : Type u} [integral_domain R] {x y : R} :
polynomial.root_multiplicity x (polynomial.X - ⇑polynomial.C y) = ite (x = y) 1 0

source
theorem polynomial.root_multiplicity_X_sub_C_pow {R : Type u} [integral_domain R] (a : R) (n : ℕ) :
polynomial.root_multiplicity a ((polynomial.X - ⇑polynomial.C a) ^ n) = n

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

source
theorem polynomial.root_multiplicity_of_dvd {R : Type u} [integral_domain R] {p : polynomial R} {a : R} {n : ℕ} :
p ≠ 0 → (polynomial.X - ⇑polynomial.C a) ^ n ∣ p → n ≤ polynomial.root_multiplicity a p

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

source
theorem polynomial.root_multiplicity_add {R : Type u} [integral_domain R] {p q : polynomial R} (a : R) :
p + q ≠ 0 → min (polynomial.root_multiplicity a p) (polynomial.root_multiplicity a q) ≤ polynomial.root_multiplicity a (p + q)

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

source
theorem polynomial.exists_multiset_roots {R : Type u} [integral_domain R] {p : polynomial R} :
p ≠ 0 → (∃ (s : multiset R), ↑(s.card) ≤ p.degree ∧ ∀ (a : R), multiset.count a s = polynomial.root_multiplicity a p)

source
def polynomial.roots {R : Type u} [integral_domain R] :
polynomial R → multiset R

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

Equations
source
@[simp]
theorem polynomial.roots_zero {R : Type u} [integral_domain R] :
0.roots = 0

source
theorem polynomial.card_roots {R : Type u} [integral_domain R] {p : polynomial R} :
p ≠ 0 → ↑(p.roots.card) ≤ p.degree

source
theorem polynomial.card_roots' {R : Type u} [integral_domain R] {p : polynomial R} :
p ≠ 0 → p.roots.card ≤ p.nat_degree

source
theorem polynomial.card_roots_sub_C {R : Type u} [integral_domain R] {p : polynomial R} {a : R} :
0 < p.degree → ↑((p - ⇑polynomial.C a).roots.card) ≤ p.degree

source
theorem polynomial.card_roots_sub_C' {R : Type u} [integral_domain R] {p : polynomial R} {a : R} :
0 < p.degree → (p - ⇑polynomial.C a).roots.card ≤ p.nat_degree

source
@[simp]
theorem polynomial.count_roots {R : Type u} {a : R} [integral_domain R] {p : polynomial R} :
p ≠ 0 → multiset.count a p.roots = polynomial.root_multiplicity a p

source
@[simp]
theorem polynomial.mem_roots {R : Type u} {a : R} [integral_domain R] {p : polynomial R} :
p ≠ 0 → (a ∈ p.roots ↔ p.is_root a)

source
theorem polynomial.eq_zero_of_infinite_is_root {R : Type u} [integral_domain R] (p : polynomial R) :
{x : R | p.is_root x}.infinite → p = 0

source
theorem polynomial.eq_of_infinite_eval_eq {R : Type u_1} [integral_domain R] (p q : polynomial R) :
{x : R | polynomial.eval x p = polynomial.eval x q}.infinite → p = q

source
theorem polynomial.roots_mul {R : Type u} [integral_domain R] {p q : polynomial R} :
p * q ≠ 0 → (p * q).roots = p.roots + q.roots

source
@[simp]
theorem polynomial.mem_roots_sub_C {R : Type u} [integral_domain R] {p : polynomial R} {a x : R} :
0 < p.degree → (x ∈ (p - ⇑polynomial.C a).roots ↔ polynomial.eval x p = a)

source
@[simp]
theorem polynomial.roots_X_sub_C {R : Type u} [integral_domain R] (r : R) :
(polynomial.X - ⇑polynomial.C r).roots = r ::ₘ 0

source
@[simp]
theorem polynomial.roots_C {R : Type u} [integral_domain R] (x : R) :
(⇑polynomial.C x).roots = 0

source
@[simp]
theorem polynomial.roots_one {R : Type u} [integral_domain R] :
1.roots = ∅

source
theorem polynomial.roots_list_prod {R : Type u} [integral_domain R] (L : list (polynomial R)) :
(∀ (p : polynomial R), p ∈ L → p ≠ 0) → L.prod.roots = ↑L.bind polynomial.roots

source
theorem polynomial.roots_multiset_prod {R : Type u} [integral_domain R] (m : multiset (polynomial R)) :
(∀ (p : polynomial R), p ∈ m → p ≠ 0) → m.prod.roots = m.bind polynomial.roots

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

source
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

source
theorem polynomial.card_roots_X_pow_sub_C {R : Type u} [integral_domain R] {n : ℕ} (hn : 0 < n) (a : R) :
(polynomial.X ^ n - ⇑polynomial.C a).roots.card ≤ n

source
def polynomial.nth_roots {R : Type u} [integral_domain R] :
ℕ → R → multiset R

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

Equations
source
@[simp]
theorem polynomial.mem_nth_roots {R : Type u} [integral_domain R] {n : ℕ} (hn : 0 < n) {a x : R} :
x ∈ polynomial.nth_roots n a ↔ x ^ n = a

source
@[simp]
theorem polynomial.nth_roots_zero {R : Type u} [integral_domain R] (r : R) :
polynomial.nth_roots 0 r = 0

source
theorem polynomial.card_nth_roots {R : Type u} [integral_domain R] (n : ℕ) (a : R) :
(polynomial.nth_roots n a).card ≤ n

source
def polynomial.nth_roots_finset (n : ℕ+) (R : Type u_1) [integral_domain R] :
finset R

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

Equations
source
@[simp]
theorem polynomial.mem_nth_roots_finset {R : Type u} [integral_domain R] {n : ℕ+} {x : R} :
x ∈ polynomial.nth_roots_finset n R ↔ x ^ ↑n = 1

source
theorem polynomial.coeff_comp_degree_mul_degree {R : Type u} [integral_domain R] {p q : polynomial R} :
q.nat_degree ≠ 0 → (p.comp q).coeff ((p.nat_degree) * q.nat_degree) = (p.leading_coeff) * q.leading_coeff ^ p.nat_degree

source
theorem polynomial.nat_degree_comp {R : Type u} [integral_domain R] {p q : polynomial R} :
(p.comp q).nat_degree = (p.nat_degree) * q.nat_degree

source
theorem polynomial.leading_coeff_comp {R : Type u} [integral_domain R] {p q : polynomial R} :
q.nat_degree ≠ 0 → (p.comp q).leading_coeff = (p.leading_coeff) * q.leading_coeff ^ p.nat_degree

source
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

source
@[simp]
theorem polynomial.nat_degree_coe_units {R : Type u} [integral_domain R] (u : units (polynomial R)) :
↑u.nat_degree = 0

source
theorem polynomial.zero_of_eval_zero {R : Type u} [integral_domain R] [infinite R] (p : polynomial R) :
(∀ (x : R), polynomial.eval x p = 0) → p = 0

source
theorem polynomial.funext {R : Type u} [integral_domain R] [infinite R] {p q : polynomial R} :
(∀ (r : R), polynomial.eval r p = polynomial.eval r q) → p = q

source
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

source
theorem polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [integral_domain R] (u : units (polynomial R)) :
↑u.coeff 0 ≠ 0

source
theorem polynomial.degree_eq_degree_of_associated {R : Type u} [integral_domain R] {p q : polynomial R} :
associated p q → p.degree = q.degree

source
theorem polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [integral_domain R] {p : polynomial R} (hi : irreducible p) {x : R} :
p.is_root x → p.degree = 1

source
theorem polynomial.leading_coeff_div_by_monic_of_monic {R : Type u} [integral_domain R] {p q : polynomial R} :
q.monic → q.degree ≤ p.degree → (p /ₘ q).leading_coeff = p.leading_coeff

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

source
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) :
is_unit f.leading_coeff → is_unit (polynomial.map φ f) → is_unit f

source
theorem polynomial.irreducible_of_irreducible_map {R : Type u} {S : Type v} [integral_domain R] [integral_domain S] (φ : R →+* S) (f : polynomial R) :
f.monic → irreducible (polynomial.map φ f) → irreducible 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.

source
theorem is_integral_domain.polynomial {R : Type u_1} [comm_ring R] :
is_integral_domain R → is_integral_domain (polynomial R)

Lift evidence that is_integral_domain R to is_integral_domain (polynomial R).