Theory of univariate polynomials
This file starts looking like the ring theory of $ R[X] $
theorem
polynomial.degree_pos_of_ne_zero_of_nonunit
{R : Type u}
[field R]
{p : polynomial R}
(hp0 : p ≠ 0)
(hp : ¬is_unit p) :
theorem
polynomial.monic_mul_leading_coeff_inv
{R : Type u}
[field R]
{p : polynomial R}
(h : p ≠ 0) :
(p * ⇑polynomial.C (p.leading_coeff)⁻¹).monic
theorem
polynomial.degree_mul_leading_coeff_inv
{R : Type u}
[field R]
{q : polynomial R}
(p : polynomial R)
(h : q ≠ 0) :
(p * ⇑polynomial.C (q.leading_coeff)⁻¹).degree = p.degree
theorem
polynomial.irreducible_of_monic
{R : Type u}
[field R]
{p : polynomial R}
(hp1 : p.monic)
(hp2 : p ≠ 1) :
irreducible p ↔ ∀ (f g : polynomial R), f.monic → g.monic → f * g = p → f = 1 ∨ g = 1
Division of polynomials. See polynomial.div_by_monic for more details.
Equations
- p.div q = (⇑polynomial.C (q.leading_coeff)⁻¹) * (p /ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹)
Remainder of polynomial division, see the lemma quotient_mul_add_remainder_eq_aux.
See polynomial.mod_by_monic for more details.
Equations
- p.mod q = p %ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹
@[instance]
Equations
- polynomial.has_div = {div := polynomial.div _inst_1}
@[instance]
Equations
- polynomial.has_mod = {mod := polynomial.mod _inst_1}
theorem
polynomial.div_def
{R : Type u}
[field R]
{p q : polynomial R} :
p / q = (⇑polynomial.C (q.leading_coeff)⁻¹) * (p /ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹)
theorem
polynomial.mod_def
{R : Type u}
[field R]
{p q : polynomial R} :
p % q = p %ₘ q * ⇑polynomial.C (q.leading_coeff)⁻¹
theorem
polynomial.mod_by_monic_eq_mod
{R : Type u}
[field R]
{q : polynomial R}
(p : polynomial R)
(hq : q.monic) :
theorem
polynomial.div_by_monic_eq_div
{R : Type u}
[field R]
{q : polynomial R}
(p : polynomial R)
(hq : q.monic) :
theorem
polynomial.mod_X_sub_C_eq_C_eval
{R : Type u}
[field R]
(p : polynomial R)
(a : R) :
p % (polynomial.X - ⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)
theorem
polynomial.mul_div_eq_iff_is_root
{R : Type u}
{a : R}
[field R]
{p : polynomial R} :
(polynomial.X - ⇑polynomial.C a) * (p / (polynomial.X - ⇑polynomial.C a)) = p ↔ p.is_root a
@[instance]
Equations
- polynomial.euclidean_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 := _, quotient := has_div.div polynomial.has_div, quotient_zero := _, remainder := has_mod.mod polynomial.has_mod, quotient_mul_add_remainder_eq := _, r := λ (p q : polynomial R), p.degree < q.degree, r_well_founded := _, remainder_lt := _, mul_left_not_lt := _}
@[simp]
theorem
polynomial.degree_map
{R : Type u}
{k : Type y}
[field R]
[field k]
(p : polynomial R)
(f : R →+* k) :
(polynomial.map f p).degree = p.degree
@[simp]
theorem
polynomial.nat_degree_map
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[field k]
(f : R →+* k) :
(polynomial.map f p).nat_degree = p.nat_degree
@[simp]
theorem
polynomial.leading_coeff_map
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[field k]
(f : R →+* k) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
theorem
polynomial.monic_map_iff
{R : Type u}
{k : Type y}
[field R]
[field k]
{f : R →+* k}
{p : polynomial R} :
(polynomial.map f p).monic ↔ p.monic
theorem
polynomial.is_unit_map
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[field k]
(f : R →+* k) :
is_unit (polynomial.map f p) ↔ is_unit p
theorem
polynomial.map_div
{R : Type u}
{k : Type y}
[field R]
{p q : polynomial R}
[field k]
(f : R →+* k) :
polynomial.map f (p / q) = polynomial.map f p / polynomial.map f q
theorem
polynomial.map_mod
{R : Type u}
{k : Type y}
[field R]
{p q : polynomial R}
[field k]
(f : R →+* k) :
polynomial.map f (p % q) = polynomial.map f p % polynomial.map f q
theorem
polynomial.gcd_map
{R : Type u}
{k : Type y}
[field R]
{p q : polynomial R}
[field k]
(f : R →+* k) :
euclidean_domain.gcd (polynomial.map f p) (polynomial.map f q) = polynomial.map f (euclidean_domain.gcd p q)
theorem
polynomial.eval₂_gcd_eq_zero
{R : Type u}
{k : Type y}
[field R]
[comm_semiring k]
{ϕ : R →+* k}
{f g : polynomial R}
{α : k}
(hf : polynomial.eval₂ ϕ α f = 0)
(hg : polynomial.eval₂ ϕ α g = 0) :
polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0
theorem
polynomial.eval_gcd_eq_zero
{R : Type u}
[field R]
{f g : polynomial R}
{α : R}
(hf : polynomial.eval α f = 0)
(hg : polynomial.eval α g = 0) :
polynomial.eval α (euclidean_domain.gcd f g) = 0
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}
(hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :
polynomial.eval₂ ϕ α f = 0
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}
(hα : polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0) :
polynomial.eval₂ ϕ α g = 0
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} :
polynomial.eval₂ ϕ α (euclidean_domain.gcd f g) = 0 ↔ polynomial.eval₂ ϕ α f = 0 ∧ polynomial.eval₂ ϕ α g = 0
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) :
is_coprime (polynomial.map f p) (polynomial.map f q) ↔ is_coprime p q
@[simp]
theorem
polynomial.map_eq_zero
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[field k]
(f : R →+* k) :
polynomial.map f p = 0 ↔ p = 0
theorem
polynomial.map_ne_zero
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[field k]
{f : R →+* k}
(hp : p ≠ 0) :
polynomial.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}
(hp : 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}
(h : p.degree = 1) :
∃ (x : R), p.is_root x
@[instance]
Equations
- polynomial.normalization_monoid = {norm_unit := λ (p : polynomial R), dite (p = 0) (λ (hp0 : p = 0), 1) (λ (hp0 : ¬p = 0), {val := ⇑polynomial.C (p.leading_coeff)⁻¹, inv := ⇑polynomial.C p.leading_coeff, val_inv := _, inv_val := _}), norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}
theorem
polynomial.coe_norm_unit
{R : Type u}
[field R]
{p : polynomial R}
(hp : p ≠ 0) :
↑(norm_unit p) = ⇑polynomial.C (p.leading_coeff)⁻¹
theorem
polynomial.map_dvd_map'
{R : Type u}
{k : Type y}
[field R]
[field k]
(f : R →+* k)
{x y : polynomial R} :
polynomial.map f x ∣ polynomial.map f y ↔ x ∣ y
theorem
polynomial.prime_of_degree_eq_one
{R : Type u}
[field R]
{p : polynomial R}
(hp1 : p.degree = 1) :
prime p
theorem
polynomial.irreducible_of_degree_eq_one
{R : Type u}
[field R]
{p : polynomial R}
(hp1 : p.degree = 1) :
theorem
polynomial.degree_pos_of_irreducible
{R : Type u}
[field R]
{p : polynomial R}
(hp : irreducible p) :
theorem
polynomial.pairwise_coprime_X_sub
{α : Type u}
[field α]
{I : Type v}
{s : I → α}
(H : function.injective s) :
pairwise (is_coprime on λ (i : I), polynomial.X - ⇑polynomial.C (s i))
theorem
polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero
{K : Type u_1}
[field K]
(f : polynomial K)
(a : K)
(hf' : polynomial.eval a f.derivative ≠ 0) :
is_coprime (polynomial.X - ⇑polynomial.C a) (f /ₘ (polynomial.X - ⇑polynomial.C a))
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).