Theory of univariate polynomials
This file starts looking like the ring theory of $ R[X] $
theorem
polynomial.monic_mul_leading_coeff_inv
{R : Type u}
[field R]
{p : polynomial R} :
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) :
q ≠ 0 → (p * ⇑polynomial.C (q.leading_coeff)⁻¹).degree = p.degree
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) :
theorem
polynomial.div_by_monic_eq_div
{R : Type u}
[field R]
{q : polynomial R}
(p : polynomial R) :
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.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} :
p ≠ 0 → polynomial.map f p ≠ 0
@[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} :
p ≠ 0 → ↑(normalization_monoid.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.irreducible_of_degree_eq_one
{R : Type u}
[field R]
{p : polynomial R} :
p.degree = 1 → irreducible p
theorem
polynomial.degree_pos_of_irreducible
{R : Type u}
[field R]
{p : polynomial R} :
irreducible p → 0 < p.degree
theorem
polynomial.pairwise_coprime_X_sub
{α : Type u}
[field α]
{I : Type v}
{s : I → α} :
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) :
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).