# mathlibdocumentation

data.polynomial.eval

# 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
• 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} :
p = (λ (e : ) (a : R), (f a) * x ^ e)

theorem polynomial.eval₂_eq_lift_nc {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} {x : S} :
= ((powers_hom S) x))

theorem polynomial.eval₂_congr {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {f g : R →+* S} {s t : S} {φ ψ : polynomial R} :
f = gs = tφ = ψ φ = ψ

@[simp]
theorem polynomial.eval₂_zero {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) :
0 = 0

@[simp]
theorem polynomial.eval₂_C {R : Type u} {S : Type v} {a : R} [semiring R] [semiring S] (f : R →+* S) (x : S) :
= f a

@[simp]
theorem polynomial.eval₂_X {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) :

@[simp]
theorem polynomial.eval₂_monomial {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) {n : } {r : R} :
( 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 : } :
= 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) :
(p + q) = p + q

@[simp]
theorem polynomial.eval₂_one {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) :
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) :
(bit0 p) = bit0 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) :
(bit1 p) = bit1 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} :
(s p) = g s p

@[simp]
theorem polynomial.eval₂_C_X {R : Type u} [semiring R] {p : polynomial R} :

@[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 : ) :
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 → ) (x : S) :
g) = (λ (n : ) (a : T), (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 : ι → ) (x : S) :
(∑ (i : ι) in s, g i) = ∑ (i : ι) in s, (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 : ∀ (k : ), commute (f (q.coeff k)) x) :
(p * q) = x p) * q

@[simp]
theorem polynomial.eval₂_mul_X {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (x : S) :
= x p) * x

@[simp]
theorem polynomial.eval₂_X_mul {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (x : S) :
= x p) * x

theorem polynomial.eval₂_mul_C' {R : Type u} {S : Type v} {a : R} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (x : S) (h : commute (f a) x) :
(p * = x p) * f a

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 : ∀ (p : , p ps∀ (k : ), commute (f (p.coeff k)) x) :
ps.prod = (list.map x) ps).prod

def polynomial.eval₂_ring_hom' {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), commute (f a) x) :

eval₂ as a ring_hom for noncommutative rings

Equations

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} (f : R →+* S) (x : S) :
(p * q) = x p) * q

theorem polynomial.eval₂_mul_eq_zero_of_left {R : Type u} {S : Type v} [semiring R] {p : polynomial R} (f : R →+* S) (x : S) (q : polynomial R) (hp : p = 0) :
(p * q) = 0

theorem polynomial.eval₂_mul_eq_zero_of_right {R : Type u} {S : Type v} [semiring R] {q : polynomial R} (f : R →+* S) (x : S) (p : polynomial R) (hq : q = 0) :
(p * q) = 0

@[instance]
def polynomial.eval₂.is_semiring_hom {R : Type u} {S : Type v} [semiring R] (f : R →+* S) (x : S) :

def polynomial.eval₂_ring_hom {R : Type u} {S : Type v} [semiring R] (f : R →+* S) (x : S) :

eval₂ as a ring_hom

Equations
@[simp]
theorem polynomial.coe_eval₂_ring_hom {R : Type u} {S : Type v} [semiring R] (f : R →+* S) (x : S) :

theorem polynomial.eval₂_pow {R : Type u} {S : Type v} [semiring R] {p : polynomial R} (f : R →+* S) (x : S) (n : ) :
(p ^ n) = p ^ n

theorem polynomial.eval₂_eq_sum_range {R : Type u} {S : Type v} [semiring R] {p : polynomial R} (f : R →+* S) (x : S) :
p = ∑ (i : ) in finset.range (p.nat_degree + 1), (f (p.coeff i)) * x ^ i

theorem polynomial.eval₂_eq_sum_range' {R : Type u} {S : Type v} [semiring R] (f : R →+* S) {p : polynomial R} {n : } (hn : p.nat_degree < n) (x : S) :
p = ∑ (i : ) in , (f (p.coeff i)) * x ^ i

def polynomial.eval {R : Type u} [semiring R] :
R → → R

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} :
= (λ (e : ) (a : R), a * x ^ e)

@[simp]
theorem polynomial.eval_C {R : Type u} {a : R} [semiring R] {x : R} :
= a

@[simp]
theorem polynomial.eval_nat_cast {R : Type u} [semiring R] {x : R} {n : } :
= n

@[simp]
theorem polynomial.eval_X {R : Type u} [semiring R] {x : R} :

@[simp]
theorem polynomial.eval_monomial {R : Type u} [semiring R] {x : R} {n : } {a : R} :
( a) = a * x ^ n

@[simp]
theorem polynomial.eval_zero {R : Type u} [semiring R] {x : R} :
= 0

@[simp]
theorem polynomial.eval_add {R : Type u} [semiring R] {p q : polynomial R} {x : R} :
(p + q) = +

@[simp]
theorem polynomial.eval_one {R : Type u} [semiring R] {x : R} :
= 1

@[simp]
theorem polynomial.eval_bit0 {R : Type u} [semiring R] {p : polynomial R} {x : R} :
(bit0 p) = bit0 p)

@[simp]
theorem polynomial.eval_bit1 {R : Type u} [semiring R] {p : polynomial R} {x : R} :
(bit1 p) = bit1 p)

@[simp]
theorem polynomial.eval_smul {R : Type u} [semiring R] (p : polynomial R) (x : R) {s : R} :
(s p) = s

theorem polynomial.eval_sum {R : Type u} [semiring R] (p : polynomial R) (f : R → ) (x : R) :
f) = (λ (n : ) (a : R), (f n a))

theorem polynomial.eval_finset_sum {R : Type u} {ι : Type y} [semiring R] (s : finset ι) (g : ι → ) (x : R) :
(∑ (i : ι) in s, g i) = ∑ (i : ι) in s, (g i)

def polynomial.is_root {R : Type u} [semiring R] (p : polynomial R) (a : R) :
Prop

is_root p x implies x is a root of p. The evaluation of p at x is zero

Equations
@[instance]
def polynomial.is_root.decidable {R : Type u} {a : R} [semiring R] {p : polynomial R} [decidable_eq R] :

Equations
@[simp]
theorem polynomial.is_root.def {R : Type u} {a : R} [semiring R] {p : polynomial R} :
p.is_root a = 0

theorem polynomial.coeff_zero_eq_eval_zero {R : Type u} [semiring R] (p : polynomial R) :
p.coeff 0 =

theorem polynomial.zero_is_root_of_coeff_zero_eq_zero {R : Type u} [semiring R] {p : polynomial R} (hp : p.coeff 0 = 0) :

def polynomial.comp {R : Type u} [semiring R] (p q : polynomial R) :

The composition of polynomials as a polynomial.

Equations
theorem polynomial.comp_eq_sum_left {R : Type u} [semiring R] {p q : polynomial R} :
p.comp q = (λ (e : ) (a : R), * q ^ e)

@[simp]
theorem polynomial.comp_X {R : Type u} [semiring R] {p : polynomial R} :

@[simp]
theorem polynomial.X_comp {R : Type u} [semiring R] {p : polynomial R} :

@[simp]
theorem polynomial.comp_C {R : Type u} {a : R} [semiring R] {p : polynomial R} :
p.comp =

@[simp]
theorem polynomial.C_comp {R : Type u} {a : R} [semiring R] {p : polynomial R} :
.comp p =

@[simp]
theorem polynomial.comp_zero {R : Type u} [semiring R] {p : polynomial R} :
p.comp 0 =

@[simp]
theorem polynomial.zero_comp {R : Type u} [semiring R] {p : polynomial R} :
0.comp p = 0

@[simp]
theorem polynomial.comp_one {R : Type u} [semiring R] {p : polynomial R} :
p.comp 1 =

@[simp]
theorem polynomial.one_comp {R : Type u} [semiring R] {p : polynomial R} :
1.comp p = 1

@[simp]
theorem polynomial.add_comp {R : Type u} [semiring R] {p q r : polynomial R} :
(p + q).comp r = p.comp r + q.comp r

@[simp]
theorem polynomial.mul_comp {R : Type u_1} (p q r : polynomial R) :
(p * q).comp r = (p.comp r) * q.comp r

@[simp]
theorem polynomial.bit0_comp {R : Type u} [semiring R] {p q : polynomial R} :
(bit0 p).comp q = bit0 (p.comp q)

@[simp]
theorem polynomial.bit1_comp {R : Type u} [semiring R] {p q : polynomial R} :
(bit1 p).comp q = bit1 (p.comp q)

theorem polynomial.comp_assoc {R : Type u_1} (φ ψ χ : polynomial R) :
(φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

def polynomial.map {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

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) :

@[simp]
theorem polynomial.map_X {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

@[simp]
theorem polynomial.map_monomial {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) {n : } {a : R} :
( a) = (f a)

@[simp]
theorem polynomial.map_zero {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
= 0

@[simp]
theorem polynomial.map_add {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) :
(p + q) = +

@[simp]
theorem polynomial.map_one {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
= 1

@[simp]
theorem polynomial.map_nat_cast {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (n : ) :
= n

@[simp]
theorem polynomial.coeff_map {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (n : ) :
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) :
p) = polynomial.map (g.comp f) p

@[simp]
theorem polynomial.map_id {R : Type u} [semiring R] {p : polynomial R} :
= 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} :
p = 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_surjective {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (hf : function.surjective 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) :
= 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] :
0

@[simp]
theorem polynomial.map_mul {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) :
(p * q) = p) *

@[instance]
def polynomial.map.is_semiring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

def polynomial.map_ring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

polynomial.map as a ring_hom

Equations
@[simp]
theorem polynomial.coe_map_ring_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)) :
= L).prod

@[simp]
theorem polynomial.map_pow {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (n : ) :
(p ^ n) = ^ n

theorem polynomial.mem_map_range {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) {p : polynomial S} :
p ∀ (n : ), p.coeff n

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) :
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) :
p) = p

theorem polynomial.map_sum {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) {ι : Type u_1} (g : ι → ) (s : finset ι) :
(∑ (i : ι) in s, g i) = ∑ (i : ι) in s, (g i)

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) (f : R →+* S) (g : S →+* T) (x : S) :
g x p) = polynomial.eval₂ (g.comp f) (g x) p

@[simp]
theorem polynomial.eval_mul {R : Type u} {p q : polynomial R} {x : R} :
(p * q) = p) *

@[instance]
def polynomial.eval.is_semiring_hom {R : Type u} {x : R} :

@[simp]
theorem polynomial.eval_pow {R : Type u} {p : polynomial R} {x : R} (n : ) :
(p ^ n) = ^ n

theorem polynomial.eval₂_hom {R : Type u} {S : Type v} {p : polynomial R} (f : R →+* S) (x : R) :
(f x) p = f p)

theorem polynomial.root_mul_left_of_is_root {R : Type u} {a : R} (p : polynomial R) {q : polynomial R} :
q.is_root a(p * q).is_root a

theorem polynomial.root_mul_right_of_is_root {R : Type u} {a : R} {p : polynomial R} (q : polynomial R) :
p.is_root a(p * q).is_root a

theorem polynomial.eval_prod {R : Type u} {ι : Type u_1} (s : finset ι) (p : ι → ) (x : R) :
(∏ (j : ι) in s, p j) = ∏ (j : ι) in s, (p j)

Polynomial evaluation commutes with finset.prod

theorem polynomial.map_multiset_prod {R : Type u} {S : Type v} (f : R →+* S) (m : multiset (polynomial R)) :
= m).prod

theorem polynomial.map_prod {R : Type u} {S : Type v} (f : R →+* S) {ι : Type u_1} (g : ι → ) (s : finset ι) :
(∏ (i : ι) in s, g i) = ∏ (i : ι) in s, (g i)

theorem polynomial.support_map_subset {R : Type u} {S : Type v} (f : R →+* S) (p : polynomial R) :

theorem polynomial.map_comp {R : Type u} {S : Type v} (f : R →+* S) (p q : polynomial R) :
(p.comp q) = p).comp q)

theorem polynomial.C_neg {R : Type u} {a : R} [ring R] :

theorem polynomial.C_sub {R : Type u} {a b : R} [ring R] :

@[instance]
def polynomial.map.is_ring_hom {R : Type u} [ring R] {S : Type u_1} [ring S] (f : R →+* S) :

@[simp]
theorem polynomial.map_sub {R : Type u} [ring R] {p q : polynomial R} {S : Type u_1} [ring S] (f : R →+* S) :
(p - q) = -

@[simp]
theorem polynomial.map_neg {R : Type u} [ring R] {p : polynomial R} {S : Type u_1} [ring S] (f : R →+* S) :
(-p) = -

@[simp]
theorem polynomial.map_int_cast {R : Type u} [ring R] {S : Type u_1} [ring S] (f : R →+* S) (n : ) :
= n

@[simp]
theorem polynomial.eval_int_cast {R : Type u} [ring R] {n : } {x : R} :
= n

@[simp]
theorem polynomial.eval₂_neg {R : Type u} [ring R] {p : polynomial R} {S : Type u_1} [ring S] (f : R →+* S) {x : S} :
(-p) = - 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} :
(p - q) = p - q

@[simp]
theorem polynomial.eval_neg {R : Type u} [ring R] (p : polynomial R) (x : R) :
(-p) = -

@[simp]
theorem polynomial.eval_sub {R : Type u} [ring R] (p q : polynomial R) (x : R) :
(p - q) = -

theorem polynomial.root_X_sub_C {R : Type u} {a b : R} [ring R] :
a = b

@[simp]
theorem polynomial.neg_comp {R : Type u} [ring R] {p q : polynomial R} :
(-p).comp q = -p.comp q

@[simp]
theorem polynomial.sub_comp {R : Type u} [ring R] {p q r : polynomial R} :
(p - q).comp r = p.comp r - q.comp r

@[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} :

@[instance]
def polynomial.eval.is_ring_hom {R : Type u} [comm_ring R] {x : R} :