Theory of univariate polynomials
The main defs here are eval₂, eval, and map.
We give several lemmas about their interaction with each other and with module operations.
def
polynomial.eval₂
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S)
(p : polynomial R) :
S
Evaluate a polynomial p given a ring hom f from the scalar ring
to the target and a value x for the variable in the target
Equations
- polynomial.eval₂ f x p = finsupp.sum p (λ (e : ℕ) (a : R), (⇑f a) * x ^ e)
theorem
polynomial.eval₂_eq_sum
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
{f : R →+* S}
{x : S} :
polynomial.eval₂ f x p = finsupp.sum p (λ (e : ℕ) (a : R), (⇑f a) * x ^ e)
@[simp]
theorem
polynomial.eval₂_zero
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x 0 = 0
@[simp]
theorem
polynomial.eval₂_C
{R : Type u}
{S : Type v}
{a : R}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x (⇑polynomial.C a) = ⇑f a
@[simp]
theorem
polynomial.eval₂_X
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x polynomial.X = x
@[simp]
theorem
polynomial.eval₂_monomial
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S)
{n : ℕ}
{r : R} :
polynomial.eval₂ f x (polynomial.monomial n r) = (⇑f r) * x ^ n
@[simp]
theorem
polynomial.eval₂_X_pow
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S)
{n : ℕ} :
polynomial.eval₂ f x (polynomial.X ^ n) = x ^ n
@[simp]
theorem
polynomial.eval₂_add
{R : Type u}
{S : Type v}
[semiring R]
{p q : polynomial R}
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x (p + q) = polynomial.eval₂ f x p + polynomial.eval₂ f x q
@[simp]
theorem
polynomial.eval₂_one
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x 1 = 1
@[simp]
theorem
polynomial.eval₂_bit0
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x (bit0 p) = bit0 (polynomial.eval₂ f x p)
@[simp]
theorem
polynomial.eval₂_bit1
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x (bit1 p) = bit1 (polynomial.eval₂ f x p)
@[simp]
theorem
polynomial.eval₂_smul
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(g : R →+* S)
(p : polynomial R)
(x : S)
{s : R} :
polynomial.eval₂ g x (s • p) = ⇑g s • polynomial.eval₂ g x p
@[instance]
def
polynomial.eval₂.is_add_monoid_hom
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S) :
@[simp]
theorem
polynomial.eval₂_nat_cast
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S)
(n : ℕ) :
polynomial.eval₂ f x ↑n = ↑n
theorem
polynomial.eval₂_sum
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
[semiring S]
(f : R →+* S)
[semiring T]
(p : polynomial T)
(g : ℕ → T → polynomial R)
(x : S) :
polynomial.eval₂ f x (finsupp.sum p g) = finsupp.sum p (λ (n : ℕ) (a : T), polynomial.eval₂ f x (g n a))
theorem
polynomial.eval₂_finset_sum
{R : Type u}
{S : Type v}
{ι : Type y}
[semiring R]
[semiring S]
(f : R →+* S)
(s : finset ι)
(g : ι → polynomial R)
(x : S) :
polynomial.eval₂ f x (∑ (i : ι) in s, g i) = ∑ (i : ι) in s, polynomial.eval₂ f x (g i)
theorem
polynomial.eval₂_mul_noncomm
{R : Type u}
{S : Type v}
[semiring R]
{p q : polynomial R}
[semiring S]
(f : R →+* S)
(x : S)
(hf : ∀ (b : R) (a : S), (⇑f b) * a = a * ⇑f b) :
polynomial.eval₂ f x (p * q) = (polynomial.eval₂ f x p) * polynomial.eval₂ f x q
theorem
polynomial.eval₂_list_prod_noncomm
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(x : S)
(ps : list (polynomial R))
(hf : ∀ (b : R) (a : S), (⇑f b) * a = a * ⇑f b) :
polynomial.eval₂ f x ps.prod = (list.map (polynomial.eval₂ f x) ps).prod
def
polynomial.eval₂_ring_hom'
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(hf : ∀ (b : R) (a : S), (⇑f b) * a = a * ⇑f b)
(x : S) :
polynomial R →+* S
eval₂ as a ring_hom for noncommutative rings
Equations
- polynomial.eval₂_ring_hom' f hf x = {to_fun := polynomial.eval₂ f x, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
We next prove that eval₂ is multiplicative as long as target ring is commutative (even if the source ring is not).
@[simp]
theorem
polynomial.eval₂_mul
{R : Type u}
{S : Type v}
[semiring R]
{p q : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x (p * q) = (polynomial.eval₂ f x p) * polynomial.eval₂ f x q
theorem
polynomial.eval₂_mul_eq_zero_of_left
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : S)
(q : polynomial R)
(hp : polynomial.eval₂ f x p = 0) :
polynomial.eval₂ f x (p * q) = 0
theorem
polynomial.eval₂_mul_eq_zero_of_right
{R : Type u}
{S : Type v}
[semiring R]
{q : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : S)
(p : polynomial R)
(hq : polynomial.eval₂ f x q = 0) :
polynomial.eval₂ f x (p * q) = 0
@[instance]
def
polynomial.eval₂.is_semiring_hom
{R : Type u}
{S : Type v}
[semiring R]
[comm_semiring S]
(f : R →+* S)
(x : S) :
def
polynomial.eval₂_ring_hom
{R : Type u}
{S : Type v}
[semiring R]
[comm_semiring S]
(f : R →+* S)
(x : S) :
polynomial R →+* S
eval₂ as a ring_hom
Equations
@[simp]
theorem
polynomial.coe_eval₂_ring_hom
{R : Type u}
{S : Type v}
[semiring R]
[comm_semiring S]
(f : R →+* S)
(x : S) :
⇑(polynomial.eval₂_ring_hom f x) = polynomial.eval₂ f x
theorem
polynomial.eval₂_pow
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : S)
(n : ℕ) :
polynomial.eval₂ f x (p ^ n) = polynomial.eval₂ f x p ^ n
theorem
polynomial.eval₂_eq_sum_range
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval₂ f x p = ∑ (i : ℕ) in finset.range (p.nat_degree + 1), (⇑f (p.coeff i)) * x ^ i
eval x p is the evaluation of the polynomial p at x
Equations
theorem
polynomial.eval_eq_sum
{R : Type u}
[semiring R]
{p : polynomial R}
{x : R} :
polynomial.eval x p = finsupp.sum p (λ (e : ℕ) (a : R), a * x ^ e)
@[simp]
theorem
polynomial.eval_C
{R : Type u}
{a : R}
[semiring R]
{x : R} :
polynomial.eval x (⇑polynomial.C a) = a
@[simp]
theorem
polynomial.eval_nat_cast
{R : Type u}
[semiring R]
{x : R}
{n : ℕ} :
polynomial.eval x ↑n = ↑n
@[simp]
@[simp]
theorem
polynomial.eval_monomial
{R : Type u}
[semiring R]
{x : R}
{n : ℕ}
{a : R} :
polynomial.eval x (polynomial.monomial n a) = a * x ^ n
@[simp]
@[simp]
theorem
polynomial.eval_add
{R : Type u}
[semiring R]
{p q : polynomial R}
{x : R} :
polynomial.eval x (p + q) = polynomial.eval x p + polynomial.eval x q
@[simp]
@[simp]
theorem
polynomial.eval_bit0
{R : Type u}
[semiring R]
{p : polynomial R}
{x : R} :
polynomial.eval x (bit0 p) = bit0 (polynomial.eval x p)
@[simp]
theorem
polynomial.eval_bit1
{R : Type u}
[semiring R]
{p : polynomial R}
{x : R} :
polynomial.eval x (bit1 p) = bit1 (polynomial.eval x p)
@[simp]
theorem
polynomial.eval_smul
{R : Type u}
[semiring R]
(p : polynomial R)
(x : R)
{s : R} :
polynomial.eval x (s • p) = s • polynomial.eval x p
theorem
polynomial.eval_sum
{R : Type u}
[semiring R]
(p : polynomial R)
(f : ℕ → R → polynomial R)
(x : R) :
polynomial.eval x (finsupp.sum p f) = finsupp.sum p (λ (n : ℕ) (a : R), polynomial.eval x (f n a))
is_root p x implies x is a root of p. The evaluation of p at x is zero
Equations
- p.is_root a = (polynomial.eval a p = 0)
@[instance]
Equations
- polynomial.decidable = polynomial.decidable._proof_1.mpr (_inst_2 (polynomial.eval a p) 0)
@[simp]
theorem
polynomial.is_root.def
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R} :
p.is_root a ↔ polynomial.eval a p = 0
theorem
polynomial.coeff_zero_eq_eval_zero
{R : Type u}
[semiring R]
(p : polynomial R) :
p.coeff 0 = polynomial.eval 0 p
theorem
polynomial.zero_is_root_of_coeff_zero_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.coeff 0 = 0) :
p.is_root 0
The composition of polynomials as a polynomial.
Equations
- p.comp q = polynomial.eval₂ polynomial.C q p
theorem
polynomial.comp_eq_sum_left
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.comp q = finsupp.sum p (λ (e : ℕ) (a : R), (⇑polynomial.C a) * q ^ e)
@[simp]
@[simp]
@[simp]
theorem
polynomial.comp_C
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R} :
p.comp (⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)
@[simp]
theorem
polynomial.C_comp
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R} :
(⇑polynomial.C a).comp p = ⇑polynomial.C a
@[simp]
theorem
polynomial.comp_zero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.comp 0 = ⇑polynomial.C (polynomial.eval 0 p)
@[simp]
@[simp]
theorem
polynomial.comp_one
{R : Type u}
[semiring R]
{p : polynomial R} :
p.comp 1 = ⇑polynomial.C (polynomial.eval 1 p)
@[simp]
@[simp]
def
polynomial.map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(a : polynomial R) :
map f p maps a polynomial p across a ring hom f
Equations
@[instance]
def
polynomial.is_semiring_hom_C_f
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
@[simp]
theorem
polynomial.map_C
{R : Type u}
{S : Type v}
{a : R}
[semiring R]
[semiring S]
(f : R →+* S) :
polynomial.map f (⇑polynomial.C a) = ⇑polynomial.C (⇑f a)
@[simp]
@[simp]
theorem
polynomial.map_monomial
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
{n : ℕ}
{a : R} :
polynomial.map f (polynomial.monomial n a) = polynomial.monomial n (⇑f a)
@[simp]
theorem
polynomial.map_zero
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
polynomial.map f 0 = 0
@[simp]
theorem
polynomial.map_add
{R : Type u}
{S : Type v}
[semiring R]
{p q : polynomial R}
[semiring S]
(f : R →+* S) :
polynomial.map f (p + q) = polynomial.map f p + polynomial.map f q
@[simp]
theorem
polynomial.map_one
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
polynomial.map f 1 = 1
@[simp]
theorem
polynomial.map_nat_cast
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(n : ℕ) :
polynomial.map f ↑n = ↑n
@[simp]
theorem
polynomial.coeff_map
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(n : ℕ) :
(polynomial.map f p).coeff n = ⇑f (p.coeff n)
theorem
polynomial.map_map
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
[semiring S]
(f : R →+* S)
[semiring T]
(g : S →+* T)
(p : polynomial R) :
polynomial.map g (polynomial.map f p) = polynomial.map (g.comp f) p
@[simp]
theorem
polynomial.map_id
{R : Type u}
[semiring R]
{p : polynomial R} :
polynomial.map (ring_hom.id R) p = p
theorem
polynomial.eval₂_eq_eval_map
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
{x : S} :
polynomial.eval₂ f x p = polynomial.eval x (polynomial.map f p)
theorem
polynomial.map_injective
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(hf : function.injective ⇑f) :
theorem
polynomial.map_monic_eq_zero_iff
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
{f : R →+* S}
(hp : p.monic) :
polynomial.map f p = 0 ↔ ∀ (x : R), ⇑f x = 0
theorem
polynomial.map_monic_ne_zero
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
{f : R →+* S}
(hp : p.monic)
[nontrivial S] :
polynomial.map f p ≠ 0
@[simp]
theorem
polynomial.map_mul
{R : Type u}
{S : Type v}
[semiring R]
{p q : polynomial R}
[semiring S]
(f : R →+* S) :
polynomial.map f (p * q) = (polynomial.map f p) * polynomial.map f q
@[instance]
def
polynomial.map.is_semiring_hom
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
theorem
polynomial.map_list_prod
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
(L : list (polynomial R)) :
polynomial.map f L.prod = (list.map (polynomial.map f) L).prod
@[simp]
theorem
polynomial.map_pow
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(n : ℕ) :
polynomial.map f (p ^ n) = polynomial.map f p ^ n
theorem
polynomial.mem_map_range
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
{p : polynomial S} :
theorem
polynomial.eval₂_map
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
[semiring T]
(g : S →+* T)
(x : T) :
polynomial.eval₂ g x (polynomial.map f p) = polynomial.eval₂ (g.comp f) x p
theorem
polynomial.eval_map
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(x : S) :
polynomial.eval x (polynomial.map f p) = polynomial.eval₂ f x p
After having set up the basic theory of eval₂, eval, comp, and map,
we make eval₂ irreducible.
Perhaps we can make the others irreducible too?
theorem
polynomial.hom_eval₂
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
(p : polynomial R)
[comm_semiring S]
[comm_semiring T]
(f : R →+* S)
(g : S →+* T)
(x : S) :
⇑g (polynomial.eval₂ f x p) = polynomial.eval₂ (g.comp f) (⇑g x) p
@[simp]
theorem
polynomial.eval_mul
{R : Type u}
[comm_semiring R]
{p q : polynomial R}
{x : R} :
polynomial.eval x (p * q) = (polynomial.eval x p) * polynomial.eval x q
@[instance]
@[simp]
theorem
polynomial.eval_pow
{R : Type u}
[comm_semiring R]
{p : polynomial R}
{x : R}
(n : ℕ) :
polynomial.eval x (p ^ n) = polynomial.eval x p ^ n
theorem
polynomial.eval₂_hom
{R : Type u}
{S : Type v}
[comm_semiring R]
{p : polynomial R}
[comm_semiring S]
(f : R →+* S)
(x : R) :
polynomial.eval₂ f (⇑f x) p = ⇑f (polynomial.eval x p)
theorem
polynomial.root_mul_left_of_is_root
{R : Type u}
{a : R}
[comm_semiring R]
(p : polynomial R)
{q : polynomial R}
(a_1 : q.is_root a) :
theorem
polynomial.root_mul_right_of_is_root
{R : Type u}
{a : R}
[comm_semiring R]
{p : polynomial R}
(q : polynomial R)
(a_1 : p.is_root a) :
theorem
polynomial.eval_prod
{R : Type u}
[comm_semiring R]
{ι : Type u_1}
(s : finset ι)
(p : ι → polynomial R)
(x : R) :
polynomial.eval x (∏ (j : ι) in s, p j) = ∏ (j : ι) in s, polynomial.eval x (p j)
Polynomial evaluation commutes with finset.prod
theorem
polynomial.map_multiset_prod
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(m : multiset (polynomial R)) :
polynomial.map f m.prod = (multiset.map (polynomial.map f) m).prod
theorem
polynomial.map_prod
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
{ι : Type u_1}
(g : ι → polynomial R)
(s : finset ι) :
polynomial.map f (∏ (i : ι) in s, g i) = ∏ (i : ι) in s, polynomial.map f (g i)
theorem
polynomial.map_sum
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
{ι : Type u_1}
(g : ι → polynomial R)
(s : finset ι) :
polynomial.map f (∑ (i : ι) in s, g i) = ∑ (i : ι) in s, polynomial.map f (g i)
theorem
polynomial.support_map_subset
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(p : polynomial R) :
(polynomial.map f p).support ⊆ p.support
theorem
polynomial.map_comp
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(p q : polynomial R) :
polynomial.map f (p.comp q) = (polynomial.map f p).comp (polynomial.map f q)
theorem
polynomial.C_sub
{R : Type u}
{a b : R}
[ring R] :
⇑polynomial.C (a - b) = ⇑polynomial.C a - ⇑polynomial.C b
@[instance]
@[simp]
theorem
polynomial.map_sub
{R : Type u}
[ring R]
{p q : polynomial R}
{S : Type u_1}
[comm_ring S]
(f : R →+* S) :
polynomial.map f (p - q) = polynomial.map f p - polynomial.map f q
@[simp]
theorem
polynomial.map_neg
{R : Type u}
[ring R]
{p : polynomial R}
{S : Type u_1}
[comm_ring S]
(f : R →+* S) :
polynomial.map f (-p) = -polynomial.map f p
@[simp]
@[simp]
theorem
polynomial.eval₂_neg
{R : Type u}
[ring R]
{p : polynomial R}
{S : Type u_1}
[ring S]
(f : R →+* S)
{x : S} :
polynomial.eval₂ f x (-p) = -polynomial.eval₂ f x p
@[simp]
theorem
polynomial.eval₂_sub
{R : Type u}
[ring R]
{p q : polynomial R}
{S : Type u_1}
[ring S]
(f : R →+* S)
{x : S} :
polynomial.eval₂ f x (p - q) = polynomial.eval₂ f x p - polynomial.eval₂ f x q
@[simp]
theorem
polynomial.eval_neg
{R : Type u}
[ring R]
(p : polynomial R)
(x : R) :
polynomial.eval x (-p) = -polynomial.eval x p
@[simp]
theorem
polynomial.eval_sub
{R : Type u}
[ring R]
(p q : polynomial R)
(x : R) :
polynomial.eval x (p - q) = polynomial.eval x p - polynomial.eval x q
theorem
polynomial.root_X_sub_C
{R : Type u}
{a b : R}
[ring R] :
(polynomial.X - ⇑polynomial.C a).is_root b ↔ a = b
@[instance]
def
polynomial.eval₂.is_ring_hom
{R : Type u}
[comm_ring R]
{S : Type u_1}
[comm_ring S]
(f : R →+* S)
{x : S} :
is_ring_hom (polynomial.eval₂ f x)
@[instance]