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} :
⇑(polynomial.aeval z) p = 0 → (∀ (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} :
⇑(polynomial.aeval z) p = 0 → (∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) → 0 < p.degree
@[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, 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} :
p ≠ 0 → 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} :
theorem
polynomial.degree_le_mul_left
{R : Type u}
[integral_domain R]
{q : polynomial R}
(p : polynomial R) :
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
roots p noncomputably gives a finset containing all the roots of p
theorem
polynomial.card_roots'
{R : Type u}
[integral_domain R]
{p : polynomial R} :
p ≠ 0 → p.roots.card ≤ p.nat_degree
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
@[simp]
@[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)
@[simp]
theorem
polynomial.roots_X_sub_C
{R : Type u}
[integral_domain R]
(r : R) :
(polynomial.X - ⇑polynomial.C r).roots = {r}
@[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.to_finset.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.to_finset.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) :
(s.prod (λ (a : R), polynomial.X - ⇑polynomial.C a)).roots = s
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
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_1}
[integral_domain R]
{n : ℕ}
(hn : 0 < n)
{a x : R} :
x ∈ polynomial.nth_roots n a ↔ x ^ n = a
theorem
polynomial.card_nth_roots
{R : Type u_1}
[integral_domain R]
(n : ℕ)
(a : R) :
(polynomial.nth_roots n a).card ≤ n
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
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} :
q.nat_degree ≠ 0 → (p.comp q).leading_coeff = p.leading_coeff * q.leading_coeff ^ p.nat_degree
@[simp]
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.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} :
associated p q → p.degree = q.degree
theorem
polynomial.degree_eq_one_of_irreducible_of_root
{R : Type u}
[integral_domain R]
{p : polynomial R}
(hi : irreducible p)
{x : R} :
theorem
polynomial.prime_of_degree_eq_one_of_monic
{R : Type u}
[integral_domain R]
{p : polynomial R} :
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
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
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
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.
Lift evidence that is_integral_domain R to is_integral_domain (polynomial R).