Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file starts looking like the ring theory of $ R[X] $
theorem
polynomial.derivative_root_multiplicity_of_root
{R : Type u}
[comm_ring R]
[is_domain R]
[char_zero R]
{p : polynomial R}
{t : R}
(hpt : p.is_root t) :
theorem
polynomial.root_multiplicity_sub_one_le_derivative_root_multiplicity
{R : Type u}
[comm_ring R]
[is_domain R]
[char_zero R]
(p : polynomial R)
(t : R) :
@[protected, instance]
noncomputable
def
polynomial.normalization_monoid
{R : Type u}
[comm_ring R]
[is_domain R]
[normalization_monoid R] :
Equations
- polynomial.normalization_monoid = {norm_unit := λ (p : polynomial R), {val := ⇑polynomial.C ↑(normalization_monoid.norm_unit p.leading_coeff), inv := ⇑polynomial.C ↑(normalization_monoid.norm_unit p.leading_coeff)⁻¹, val_inv := _, inv_val := _}, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}
@[simp]
theorem
polynomial.coe_norm_unit
{R : Type u}
[comm_ring R]
[is_domain R]
[normalization_monoid R]
{p : polynomial R} :
theorem
polynomial.leading_coeff_normalize
{R : Type u}
[comm_ring R]
[is_domain R]
[normalization_monoid R]
(p : polynomial R) :
theorem
polynomial.monic.normalize_eq_self
{R : Type u}
[comm_ring R]
[is_domain R]
[normalization_monoid R]
{p : polynomial R}
(hp : p.monic) :
theorem
polynomial.roots_normalize
{R : Type u}
[comm_ring R]
[is_domain R]
[normalization_monoid R]
{p : polynomial R} :
theorem
polynomial.degree_pos_of_ne_zero_of_nonunit
{R : Type u}
[division_ring R]
{p : polynomial R}
(hp0 : p ≠ 0)
(hp : ¬is_unit p) :
theorem
polynomial.monic_mul_leading_coeff_inv
{R : Type u}
[division_ring R]
{p : polynomial R}
(h : p ≠ 0) :
(p * ⇑polynomial.C (p.leading_coeff)⁻¹).monic
theorem
polynomial.degree_mul_leading_coeff_inv
{R : Type u}
[division_ring R]
{q : polynomial R}
(p : polynomial R)
(h : q ≠ 0) :
(p * ⇑polynomial.C (q.leading_coeff)⁻¹).degree = p.degree
@[simp]
theorem
polynomial.map_eq_zero
{R : Type u}
{S : Type v}
[division_ring R]
{p : polynomial R}
[semiring S]
[nontrivial S]
(f : R →+* S) :
polynomial.map f p = 0 ↔ p = 0
theorem
polynomial.map_ne_zero
{R : Type u}
{S : Type v}
[division_ring R]
{p : polynomial R}
[semiring S]
[nontrivial S]
{f : R →+* S}
(hp : p ≠ 0) :
polynomial.map f p ≠ 0
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 polynomial.mod_by_monic for more details.
Equations
- p.mod q = p %ₘ (q * ⇑polynomial.C (q.leading_coeff)⁻¹)
@[protected, instance]
Equations
- polynomial.has_div = {div := polynomial.div _inst_1}
@[protected, 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
@[protected, instance]
Equations
- polynomial.euclidean_domain = {to_comm_ring := {add := comm_ring.add polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero polynomial.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul polynomial.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg polynomial.comm_ring, sub := comm_ring.sub polynomial.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul polynomial.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast polynomial.comm_ring, nat_cast := comm_ring.nat_cast polynomial.comm_ring, one := comm_ring.one polynomial.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul polynomial.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow polynomial.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := _, 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]
[division_ring 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}
[division_ring 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}
[division_ring 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]
[division_ring 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
theorem
polynomial.mem_roots_map
{R : Type u}
{k : Type y}
[field R]
{p : polynomial R}
[comm_ring k]
[is_domain 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) :
theorem
polynomial.leading_coeff_div
{R : Type u}
[field R]
{p q : polynomial R}
(hpq : q.degree ≤ p.degree) :
(p / q).leading_coeff = p.leading_coeff / q.leading_coeff
theorem
polynomial.div_C_mul
{R : Type u}
{a : R}
[field R]
{p q : polynomial R} :
p / (⇑polynomial.C a * q) = ⇑polynomial.C a⁻¹ * (p / q)
theorem
polynomial.coe_norm_unit_of_ne_zero
{R : Type u}
[field R]
{p : polynomial R}
(hp : p ≠ 0) :
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.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 (⇑polynomial.derivative f) ≠ 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).