Evaluating a polynomial

Main definitions

• Polynomial.eval₂: evaluate p : R[X] in S given a ring hom f : R →+* S and x : S.
• Polynomial.eval: evaluate p : R[X] given x : R.
• Polynomial.IsRoot: x : R is a root of p : R[X].
• Polynomial.comp: compose two polynomials p q : R[X] by evaluating p at q.
• Polynomial.map: apply f : R →+* S to the coefficients of p : R[X].

We also provide the following bundled versions:

• Polynomial.eval₂AddMonoidHom, Polynomial.eval₂RingHom
• Polynomial.evalRingHom
• Polynomial.compRingHom
• Polynomial.mapRingHom

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

• Polynomial.eval₂ f x p = p.sum fun (e : ℕ) (a : R) => f a * x ^ e

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 = g → s = 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) : Polynomial R →+ 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

• Polynomial.eval₂AddMonoidHom f x = { toFun := Polynomial.eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Polynomial.eval₂AddMonoidHom_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) : (eval₂AddMonoidHom f x) p = eval₂ f x p

@[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) : eval₂ f a (OfNat.ofNat n) = OfNat.ofNat 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) : 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) : eval₂ f x s.sum = (Multiset.map (eval₂ f x) s).sum

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 (∑ i ∈ s, g i) = ∑ i ∈ s, 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 : ∀ p ∈ ps, ∀ (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) : Polynomial R →+* S

eval₂ as a RingHom for noncommutative rings

Equations

• Polynomial.eval₂RingHom' f x hf = { toFun := Polynomial.eval₂ f x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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) : Polynomial R →+* S

eval₂ as a RingHom

Equations

• Polynomial.eval₂RingHom f x = { toFun := (↑(Polynomial.eval₂AddMonoidHom f x)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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 ∣ q → eval₂ 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] (x : R) (p : Polynomial R) : R

eval x p is the evaluation of the polynomial p at x

Equations

• Polynomial.eval x p = Polynomial.eval₂ (RingHom.id R) x p

@[simp]

theorem Polynomial.eval₂_id {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : eval₂ (RingHom.id R) x p = eval x p

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] : eval₂ f (OfNat.ofNat n) p = f (eval (OfNat.ofNat n) p)

@[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) : eval a (OfNat.ofNat n) = OfNat.ofNat n

@[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_listSum {R : Type u} [Semiring R] (l : List (Polynomial R)) (x : R) : eval x l.sum = (List.map (eval x) l).sum

Polynomial evaluation commutes with List.sum.

theorem Polynomial.eval_multisetSum {R : Type u} [Semiring R] (s : Multiset (Polynomial R)) (x : R) : eval x s.sum = (Multiset.map (eval x) s).sum

Polynomial evaluation commutes with Multiset.sum.

theorem Polynomial.eval_sum {R : Type u} [Semiring R] (p : Polynomial R) (f : ℕ → R → Polynomial 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 (∑ i ∈ s, g i) = ∑ i ∈ s, eval x (g i)

def Polynomial.IsRoot {R : Type u} [Semiring R] (p : Polynomial R) (a : R) : Prop

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

Equations

• p.IsRoot a = (Polynomial.eval a p = 0)

instance Polynomial.IsRoot.decidable {R : Type u} {a : R} [Semiring R] {p : Polynomial R} [DecidableEq R] : Decidable (p.IsRoot a)

Equations

• Polynomial.IsRoot.decidable = id inferInstance

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

theorem Polynomial.eval_surjective {R : Type u} [Semiring R] (x : R) : Function.Surjective (eval x)

def Polynomial.comp {R : Type u} [Semiring R] (p q : Polynomial R) : Polynomial R

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 = 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) : (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q

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

map f p maps a polynomial p across a ring hom f

Equations

• Polynomial.map f = Polynomial.eval₂ (Polynomial.C.comp f) Polynomial.X

@[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 R →+* Polynomial S

Polynomial.map as a RingHom.

Equations

• Polynomial.mapRingHom f = { toFun := Polynomial.map f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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] : map f (OfNat.ofNat n) = OfNat.ofNat n

theorem Polynomial.map_dvd {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {x y : Polynomial R} : x ∣ y → map 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) : (mapRingHom f).comp C = C.comp f

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 (∑ i ∈ s, g i) = ∑ i ∈ s, 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

def Polynomial.evalRingHom {R : Type u} [CommSemiring R] : R → Polynomial R →+* R

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

Equations

• Polynomial.evalRingHom = Polynomial.eval₂RingHom (RingHom.id R)

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

theorem Polynomial.eval_X_pow {R : Type u} [CommSemiring R] {x : R} (n : ℕ) : eval x (X ^ n) = x ^ 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)

def Polynomial.compRingHom {R : Type u} [CommSemiring R] : Polynomial R → Polynomial R →+* Polynomial R

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

Equations

• Polynomial.compRingHom = Polynomial.eval₂RingHom Polynomial.C

@[simp]

theorem Polynomial.coe_compRingHom {R : Type u} [CommSemiring R] (q : Polynomial R) : ⇑q.compRingHom = fun (p : Polynomial R) => p.comp q

theorem Polynomial.coe_compRingHom_apply {R : Type u} [CommSemiring R] (p q : Polynomial R) : q.compRingHom p = 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) : eval₂ f x s.prod = (Multiset.map (eval₂ f x) s).prod

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 (∏ i ∈ s, g i) = ∏ i ∈ s, 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

theorem Polynomial.eval_multiset_prod {R : Type u} [CommSemiring R] (s : Multiset (Polynomial R)) (x : R) : eval x s.prod = (Multiset.map (eval x) s).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 (∏ j ∈ s, p j) = ∏ j ∈ s, 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) : (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q

theorem Polynomial.isRoot_prod {R : Type u_2} [CommSemiring R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R) : (∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x

theorem Polynomial.eval_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} : p ∣ q → eval 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 ∣ q → eval x p = 0 → eval x q = 0

@[simp]

theorem Polynomial.eval_geom_sum {R : Type u_1} [CommSemiring R] {n : ℕ} {x : R} : eval x (∑ i ∈ Finset.range n, X ^ i) = ∑ i ∈ Finset.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)) : map f m.prod = (Multiset.map (map f) m).prod

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 (∏ i ∈ s, g i) = ∏ i ∈ s, 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)