Documentation

Mathlib.Algebra.Polynomial.Eval.Defs

Evaluating a polynomial #

Main definitions #

We also provide the following bundled versions:

We include results on applying the definitions to C, X and ring operations.

@[irreducible]
def Polynomial.eval₂ {R : Type u_1} {S : Type u_2} [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
theorem Polynomial.eval₂_def {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) :
eval₂ f x p = p.sum fun (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} :
eval₂ f x p = p.sum fun (e : ) (a : R) => f a * x ^ e
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φ = ψeval₂ f s φ = eval₂ g t ψ
@[simp]
theorem Polynomial.eval₂_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :
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) :
eval₂ f x (C a) = f a
@[simp]
theorem Polynomial.eval₂_X {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :
eval₂ f x 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} :
eval₂ f x ((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 : } :
eval₂ f x (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) :
eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q
@[simp]
theorem Polynomial.eval₂_one {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :
eval₂ f x 1 = 1
def Polynomial.eval₂AddMonoidHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :

eval₂AddMonoidHom (f : R →+* S) (x : S) is the AddMonoidHom from R[X] to S obtained by evaluating the pushforward of p along f at x.

Equations
@[simp]
theorem Polynomial.eval₂AddMonoidHom_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) :
@[simp]
theorem Polynomial.eval₂_natCast {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (n : ) :
eval₂ f x n = n
@[simp]
theorem Polynomial.eval₂_ofNat {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] (n : ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
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 : TPolynomial R) (x : S) :
eval₂ f x (p.sum g) = p.sum fun (n : ) (a : T) => eval₂ f x (g n a)
theorem Polynomial.eval₂_list_sum {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S) :
eval₂ f x l.sum = (List.map (eval₂ f x) l).sum
theorem Polynomial.eval₂_multiset_sum {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (s : Multiset (Polynomial R)) (x : S) :
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) :
eval₂ f x (∑ is, g i) = is, eval₂ f x (g i)
theorem Polynomial.eval₂_ofFinsupp {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {x : S} {p : AddMonoidAlgebra R } :
eval₂ f x { toFinsupp := p } = (AddMonoidAlgebra.liftNC f ((powersHom S) x)) p
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) :
eval₂ f x (p * q) = eval₂ f x p * eval₂ f x 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) :
eval₂ f x (p * X) = eval₂ f 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) :
eval₂ f x (X * p) = eval₂ f 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) :
eval₂ f x (p * C a) = eval₂ f 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 : pps, ∀ (k : ), Commute (f (p.coeff k)) x) :
eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
def Polynomial.eval₂RingHom' {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 RingHom for noncommutative rings

Equations
@[simp]
theorem Polynomial.eval₂RingHom'_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) (p : Polynomial R) :
(eval₂RingHom' f x hf) p = eval₂ f x p

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} [CommSemiring S] (f : R →+* S) (x : S) :
eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q
theorem Polynomial.eval₂_mul_eq_zero_of_left {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (q : Polynomial R) (hp : eval₂ f x p = 0) :
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} [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hq : eval₂ f x q = 0) :
eval₂ f x (p * q) = 0
def Polynomial.eval₂RingHom {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) :

eval₂ as a RingHom

Equations
@[simp]
theorem Polynomial.coe_eval₂RingHom {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) :
(eval₂RingHom f x) = eval₂ f x
theorem Polynomial.eval₂_pow {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (n : ) :
eval₂ f x (p ^ n) = eval₂ f x p ^ n
theorem Polynomial.eval₂_dvd {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) :
p qeval₂ f x p eval₂ f x q
theorem Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (h : p q) (h0 : eval₂ f x p = 0) :
eval₂ f x q = 0
theorem Polynomial.eval₂_list_prod {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S) :
eval₂ f x l.prod = (List.map (eval₂ f x) l).prod
def Polynomial.eval {R : Type u} [Semiring R] :
RPolynomial RR

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} :
eval x p = p.sum fun (e : ) (a : R) => a * x ^ e
@[simp]
theorem Polynomial.eval₂_at_apply {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (r : R) :
eval₂ f (f r) p = f (eval r p)
@[simp]
theorem Polynomial.eval₂_at_one {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) :
eval₂ f 1 p = f (eval 1 p)
@[simp]
theorem Polynomial.eval₂_at_natCast {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ) :
eval₂ f (↑n) p = f (eval (↑n) p)
@[simp]
theorem Polynomial.eval₂_at_ofNat {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ) [n.AtLeastTwo] :
@[simp]
theorem Polynomial.eval_C {R : Type u} {a : R} [Semiring R] {x : R} :
eval x (C a) = a
@[simp]
theorem Polynomial.eval_natCast {R : Type u} [Semiring R] {x : R} {n : } :
eval x n = n
@[simp]
theorem Polynomial.eval_ofNat {R : Type u} [Semiring R] (n : ) [n.AtLeastTwo] (a : R) :
@[simp]
theorem Polynomial.eval_X {R : Type u} [Semiring R] {x : R} :
eval x X = x
@[simp]
theorem Polynomial.eval_monomial {R : Type u} [Semiring R] {x : R} {n : } {a : R} :
eval x ((monomial n) a) = a * x ^ n
@[simp]
theorem Polynomial.eval_zero {R : Type u} [Semiring R] {x : R} :
eval x 0 = 0
@[simp]
theorem Polynomial.eval_add {R : Type u} [Semiring R] {p q : Polynomial R} {x : R} :
eval x (p + q) = eval x p + eval x q
@[simp]
theorem Polynomial.eval_one {R : Type u} [Semiring R] {x : R} :
eval x 1 = 1
@[simp]
theorem Polynomial.eval_C_mul {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {x : R} :
eval x (C a * p) = a * eval x p
@[simp]
theorem Polynomial.eval_natCast_mul {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {n : } :
eval x (n * p) = n * eval x p
@[simp]
theorem Polynomial.eval_mul_X {R : Type u} [Semiring R] {p : Polynomial R} {x : R} :
eval x (p * X) = eval x p * x
@[simp]
theorem Polynomial.eval_mul_X_pow {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {k : } :
eval x (p * X ^ k) = eval x p * x ^ k
theorem Polynomial.eval_sum {R : Type u} [Semiring R] (p : Polynomial R) (f : RPolynomial R) (x : R) :
eval x (p.sum f) = p.sum fun (n : ) (a : R) => eval x (f n a)
theorem Polynomial.eval_finset_sum {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (g : ιPolynomial R) (x : R) :
eval x (∑ is, g i) = is, eval x (g i)
def Polynomial.IsRoot {R : Type u} [Semiring R] (p : Polynomial R) (a : R) :

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

Equations
@[simp]
theorem Polynomial.IsRoot.def {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
p.IsRoot a eval a p = 0
theorem Polynomial.IsRoot.eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : R} (h : p.IsRoot x) :
eval x p = 0
theorem Polynomial.IsRoot.dvd {R : Type u_1} [CommSemiring R] {p q : Polynomial R} {x : R} (h : p.IsRoot x) (hpq : p q) :
q.IsRoot x
theorem Polynomial.not_isRoot_C {R : Type u} [Semiring R] (r a : R) (hr : r 0) :
¬(C r).IsRoot a
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 = p.sum fun (e : ) (a : R) => C a * q ^ e
@[simp]
theorem Polynomial.comp_X {R : Type u} [Semiring R] {p : Polynomial R} :
p.comp X = p
@[simp]
theorem Polynomial.X_comp {R : Type u} [Semiring R] {p : Polynomial R} :
X.comp p = p
@[simp]
theorem Polynomial.comp_C {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
p.comp (C a) = C (eval a p)
@[simp]
theorem Polynomial.C_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
(C a).comp p = C a
@[simp]
theorem Polynomial.natCast_comp {R : Type u} [Semiring R] {p : Polynomial R} {n : } :
(↑n).comp p = n
@[simp]
theorem Polynomial.ofNat_comp {R : Type u} [Semiring R] {p : Polynomial R} (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).comp p = n
@[simp]
theorem Polynomial.comp_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.comp 0 = C (eval 0 p)
@[simp]
theorem Polynomial.zero_comp {R : Type u} [Semiring R] {p : Polynomial R} :
comp 0 p = 0
@[simp]
theorem Polynomial.comp_one {R : Type u} [Semiring R] {p : Polynomial R} :
p.comp 1 = C (eval 1 p)
@[simp]
theorem Polynomial.one_comp {R : Type u} [Semiring R] {p : Polynomial R} :
comp 1 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.monomial_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ) :
((monomial n) a).comp p = C a * p ^ n
@[simp]
theorem Polynomial.mul_X_comp {R : Type u} [Semiring R] {p r : Polynomial R} :
(p * X).comp r = p.comp r * r
@[simp]
theorem Polynomial.X_pow_comp {R : Type u} [Semiring R] {p : Polynomial R} {k : } :
(X ^ k).comp p = p ^ k
@[simp]
theorem Polynomial.mul_X_pow_comp {R : Type u} [Semiring R] {p r : Polynomial R} {k : } :
(p * X ^ k).comp r = p.comp r * r ^ k
@[simp]
theorem Polynomial.C_mul_comp {R : Type u} {a : R} [Semiring R] {p r : Polynomial R} :
(C a * p).comp r = C a * p.comp r
@[simp]
theorem Polynomial.natCast_mul_comp {R : Type u} [Semiring R] {p r : Polynomial R} {n : } :
(n * p).comp r = n * p.comp r
theorem Polynomial.mul_X_add_natCast_comp {R : Type u} [Semiring R] {p q : Polynomial R} {n : } :
(p * (X + n)).comp q = p.comp q * (q + n)
@[simp]
theorem Polynomial.mul_comp {R : Type u_1} [CommSemiring R] (p q r : Polynomial R) :
(p * q).comp r = p.comp r * q.comp r
@[simp]
theorem Polynomial.pow_comp {R : Type u_1} [CommSemiring R] (p q : Polynomial R) (n : ) :
(p ^ n).comp q = p.comp q ^ n
theorem Polynomial.comp_assoc {R : Type u_1} [CommSemiring R] (φ ψ χ : Polynomial R) :
(φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
@[simp]
theorem Polynomial.sum_comp {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (p : ιPolynomial R) (q : Polynomial R) :
(∑ is, p i).comp q = is, (p i).comp q
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
@[simp]
theorem Polynomial.map_C {R : Type u} {S : Type v} {a : R} [Semiring R] [Semiring S] (f : R →+* S) :
map f (C a) = C (f a)
@[simp]
theorem Polynomial.map_X {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
map f X = X
@[simp]
theorem Polynomial.map_monomial {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {n : } {a : R} :
map f ((monomial n) a) = (monomial n) (f a)
@[simp]
theorem Polynomial.map_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
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) :
map f (p + q) = map f p + map f q
@[simp]
theorem Polynomial.map_one {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
map f 1 = 1
@[simp]
theorem Polynomial.map_mul {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) :
map f (p * q) = map f p * map f q
def Polynomial.mapRingHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :

Polynomial.map as a RingHom.

Equations
@[simp]
theorem Polynomial.coe_mapRingHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
(mapRingHom f) = map f
@[simp]
theorem Polynomial.map_natCast {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ) :
map f n = n
@[simp]
theorem Polynomial.map_ofNat {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ) [n.AtLeastTwo] :
theorem Polynomial.map_dvd {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {x y : Polynomial R} :
x ymap f x map f y
theorem Polynomial.mapRingHom_comp_C {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) :
theorem Polynomial.eval₂_eq_eval_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) {x : S} :
eval₂ f x p = eval x (map f p)
theorem Polynomial.map_list_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (L : List (Polynomial R)) :
map f L.prod = (List.map (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 : ) :
map f (p ^ n) = map f p ^ n
theorem Polynomial.eval_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
eval x (map f p) = eval₂ f x p
theorem Polynomial.map_sum {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {ι : Type u_1} (g : ιPolynomial R) (s : Finset ι) :
map f (∑ is, g i) = is, map f (g i)
theorem Polynomial.map_comp {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p q : Polynomial R) :
map f (p.comp q) = (map f p).comp (map f q)
@[simp]
theorem Polynomial.eval_mul {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} :
eval x (p * q) = eval x p * eval x q

eval r, regarded as a ring homomorphism from R[X] to R.

Equations
@[simp]
theorem Polynomial.coe_evalRingHom {R : Type u} [CommSemiring R] (r : R) :
(evalRingHom r) = eval r
@[simp]
theorem Polynomial.eval_pow {R : Type u} [CommSemiring R] {p : Polynomial R} {x : R} (n : ) :
eval x (p ^ n) = eval x p ^ n
@[simp]
theorem Polynomial.eval_comp {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} :
eval x (p.comp q) = eval (eval x q) p
theorem Polynomial.isRoot_comp {R : Type u_1} [CommSemiring R] {p q : Polynomial R} {r : R} :
(p.comp q).IsRoot r p.IsRoot (eval r q)

comp p, regarded as a ring homomorphism from R[X] to itself.

Equations
@[simp]
theorem Polynomial.coe_compRingHom {R : Type u} [CommSemiring R] (q : Polynomial R) :
q.compRingHom = fun (p : Polynomial R) => p.comp q
theorem Polynomial.root_mul_left_of_isRoot {R : Type u} {a : R} [CommSemiring R] (p : Polynomial R) {q : Polynomial R} :
q.IsRoot a(p * q).IsRoot a
theorem Polynomial.root_mul_right_of_isRoot {R : Type u} {a : R} [CommSemiring R] {p : Polynomial R} (q : Polynomial R) :
p.IsRoot a(p * q).IsRoot a
theorem Polynomial.eval₂_multiset_prod {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Multiset (Polynomial R)) (x : S) :
theorem Polynomial.eval₂_finset_prod {R : Type u} {S : Type v} {ι : Type y} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Finset ι) (g : ιPolynomial R) (x : S) :
eval₂ f x (∏ is, g i) = is, eval₂ f x (g i)
theorem Polynomial.eval_list_prod {R : Type u} [CommSemiring R] (l : List (Polynomial R)) (x : R) :
eval x l.prod = (List.map (eval x) l).prod

Polynomial evaluation commutes with List.prod

Polynomial evaluation commutes with Multiset.prod

theorem Polynomial.eval_prod {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (x : R) :
eval x (∏ js, p j) = js, eval x (p j)

Polynomial evaluation commutes with Finset.prod

theorem Polynomial.list_prod_comp {R : Type u} [CommSemiring R] (l : List (Polynomial R)) (q : Polynomial R) :
l.prod.comp q = (List.map (fun (p : Polynomial R) => p.comp q) l).prod
theorem Polynomial.multiset_prod_comp {R : Type u} [CommSemiring R] (s : Multiset (Polynomial R)) (q : Polynomial R) :
s.prod.comp q = (Multiset.map (fun (p : Polynomial R) => p.comp q) s).prod
theorem Polynomial.prod_comp {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (q : Polynomial R) :
(∏ js, p j).comp q = js, (p j).comp q
theorem Polynomial.isRoot_prod {R : Type u_2} [CommRing R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (x : R) :
(∏ js, p j).IsRoot x is, (p i).IsRoot x
theorem Polynomial.eval_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} :
p qeval x p eval x q
theorem Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} :
p qeval x p = 0eval x q = 0
@[simp]
theorem Polynomial.eval_geom_sum {R : Type u_1} [CommSemiring R] {n : } {x : R} :
eval x (∑ iFinset.range n, X ^ i) = iFinset.range n, x ^ i
theorem Polynomial.root_mul {R : Type u} {a : R} [CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R] :
(p * q).IsRoot a p.IsRoot a q.IsRoot a
theorem Polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [CommSemiring R] {p q : Polynomial R} [NoZeroDivisors R] (h : (p * q).IsRoot a) :
p.IsRoot a q.IsRoot a
theorem Polynomial.map_multiset_prod {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (m : Multiset (Polynomial R)) :
theorem Polynomial.map_prod {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) {ι : Type u_1} (g : ιPolynomial R) (s : Finset ι) :
map f (∏ is, g i) = is, map f (g i)
@[simp]
theorem Polynomial.map_sub {R : Type u} [Ring R] {p q : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) :
map f (p - q) = map f p - map f q
@[simp]
theorem Polynomial.map_neg {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) :
map f (-p) = -map f p
@[simp]
theorem Polynomial.map_intCast {R : Type u} [Ring R] {S : Type u_1} [Ring S] (f : R →+* S) (n : ) :
map f n = n
@[simp]
theorem Polynomial.eval_intCast {R : Type u} [Ring R] {n : } {x : R} :
eval x n = 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} :
eval₂ f x (-p) = -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} :
eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
@[simp]
theorem Polynomial.eval_neg {R : Type u} [Ring R] (p : Polynomial R) (x : R) :
eval x (-p) = -eval x p
@[simp]
theorem Polynomial.eval_sub {R : Type u} [Ring R] (p q : Polynomial R) (x : R) :
eval x (p - q) = eval x p - eval x q
theorem Polynomial.root_X_sub_C {R : Type u} {a b : R} [Ring R] :
(X - C a).IsRoot b 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
@[simp]
theorem Polynomial.intCast_comp {R : Type u} [Ring R] {p : Polynomial R} (i : ) :
(↑i).comp p = i
@[simp]
theorem Polynomial.eval₂_at_intCast {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) (n : ) :
eval₂ f (↑n) p = f (eval (↑n) p)
theorem Polynomial.mul_X_sub_intCast_comp {R : Type u} [Ring R] {p q : Polynomial R} {n : } :
(p * (X - n)).comp q = p.comp q * (q - n)