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 = 0 → x = 0) :
0 < p.nat_degree
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 = 0 → x = 0) :
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) :
⇑(polynomial.aeval x) (p %ₘ q) = ⇑(polynomial.aeval x) p
@[instance]
Equations
- polynomial.integral_domain = {add := comm_ring.add polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero polynomial.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg polynomial.comm_ring, sub := comm_ring.sub polynomial.comm_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul polynomial.comm_ring, mul_assoc := _, one := comm_ring.one polynomial.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
theorem
polynomial.nat_degree_mul
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(hp : p ≠ 0)
(hq : q ≠ 0) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
@[simp]
theorem
polynomial.nat_degree_pow
{R : Type u}
[integral_domain R]
(p : polynomial R)
(n : ℕ) :
(p ^ n).nat_degree = n * p.nat_degree
theorem
polynomial.root_or_root_of_root_mul
{R : Type u}
{a : R}
[integral_domain R]
{p q : polynomial R}
(h : (p * q).is_root a) :
theorem
polynomial.degree_le_mul_left
{R : Type u}
[integral_domain R]
{q : polynomial R}
(p : polynomial R)
(hq : q ≠ 0) :
theorem
polynomial.nat_degree_le_of_dvd
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(h1 : p ∣ q)
(h2 : q ≠ 0) :
p.nat_degree ≤ q.nat_degree
theorem
polynomial.degree_eq_zero_of_is_unit
{R : Type u}
[integral_domain R]
{p : polynomial R}
(h : is_unit p) :
@[simp]
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) :
prime p
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_eq_zero
{R : Type u}
[integral_domain R]
{p : polynomial R}
{x : R}
(h : ¬p.is_root x) :
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
theorem
polynomial.root_multiplicity_mul
{R : Type u}
[integral_domain R]
{p q : polynomial R}
{x : R}
(hpq : p * q ≠ 0) :
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
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.
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.
theorem
polynomial.root_multiplicity_add
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(a : R)
(hzero : 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.
theorem
polynomial.exists_multiset_roots
{R : Type u}
[integral_domain R]
{p : polynomial R}
(hp : p ≠ 0) :
∃ (s : multiset R), ↑(⇑multiset.card s) ≤ p.degree ∧ ∀ (a : R), multiset.count a s = polynomial.root_multiplicity a p
roots p noncomputably gives a multiset containing all the roots of p,
including their multiplicities.
theorem
polynomial.card_roots_sub_C
{R : Type u}
[integral_domain R]
{p : polynomial R}
{a : R}
(hp0 : 0 < p.degree) :
↑(⇑multiset.card (p - ⇑polynomial.C a).roots) ≤ p.degree
theorem
polynomial.card_roots_sub_C'
{R : Type u}
[integral_domain R]
{p : polynomial R}
{a : R}
(hp0 : 0 < p.degree) :
⇑multiset.card (p - ⇑polynomial.C a).roots ≤ p.nat_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.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) :
@[simp]
theorem
polynomial.mem_roots_sub_C
{R : Type u}
[integral_domain R]
{p : polynomial R}
{a x : R}
(hp0 : 0 < p.degree) :
x ∈ (p - ⇑polynomial.C a).roots ↔ polynomial.eval x p = a
@[simp]
theorem
polynomial.roots_X_sub_C
{R : Type u}
[integral_domain R]
(r : R) :
(polynomial.X - ⇑polynomial.C r).roots = r ::ₘ 0
@[simp]
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
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
theorem
polynomial.roots_prod
{R : Type u}
[integral_domain R]
{ι : Type u_1}
(f : ι → polynomial R)
(s : finset ι) :
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) :
⇑multiset.card (polynomial.X ^ n - ⇑polynomial.C a).roots ≤ n
nth_roots n a noncomputably returns the solutions to x ^ n = a
Equations
- polynomial.nth_roots n a = (polynomial.X ^ n - ⇑polynomial.C a).roots
@[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
@[simp]
theorem
polynomial.nth_roots_zero
{R : Type u}
[integral_domain R]
(r : R) :
polynomial.nth_roots 0 r = 0
theorem
polynomial.card_nth_roots
{R : Type u}
[integral_domain R]
(n : ℕ)
(a : R) :
⇑multiset.card (polynomial.nth_roots n a) ≤ n
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} :
x ∈ polynomial.nth_roots_finset n R ↔ x ^ n = 1
theorem
polynomial.coeff_comp_degree_mul_degree
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(hqd0 : q.nat_degree ≠ 0) :
(p.comp q).coeff ((p.nat_degree) * q.nat_degree) = (p.leading_coeff) * q.leading_coeff ^ p.nat_degree
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
theorem
polynomial.leading_coeff_comp
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(hq : q.nat_degree ≠ 0) :
(p.comp q).leading_coeff = (p.leading_coeff) * q.leading_coeff ^ p.nat_degree
theorem
polynomial.units_coeff_zero_smul
{R : Type u}
[integral_domain R]
(c : units (polynomial R))
(p : polynomial R) :
@[simp]
theorem
polynomial.nat_degree_coe_units
{R : Type u}
[integral_domain R]
(u : units (polynomial R)) :
↑u.nat_degree = 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
theorem
polynomial.coeff_coe_units_zero_ne_zero
{R : Type u}
[integral_domain R]
(u : units (polynomial R)) :
theorem
polynomial.degree_eq_degree_of_associated
{R : Type u}
[integral_domain R]
{p q : polynomial R}
(h : associated p q) :
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) :
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) :
(p /ₘ q).leading_coeff = p.leading_coeff
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)) :
is_unit 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.
Lift evidence that is_integral_domain R to is_integral_domain (polynomial R).