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) : Polynomial.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} : Polynomial.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 → φ = ψ → Polynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ

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

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) : (Polynomial.eval₂AddMonoidHom f x) p = Polynomial.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 : ℕ) : Polynomial.eval₂ f x ↑n = ↑n

@[deprecated Polynomial.eval₂_natCast]

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

Alias of Polynomial.eval₂_natCast.

@[simp]

theorem Polynomial.eval₂_ofNat {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) : Polynomial.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) : Polynomial.eval₂ f x (p.sum g) = p.sum fun (n : ℕ) (a : T) => Polynomial.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) : Polynomial.eval₂ f x l.sum = (List.map (Polynomial.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) : Polynomial.eval₂ f x s.sum = (Multiset.map (Polynomial.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) : Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.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 ℕ} : Polynomial.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) : Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.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) : Polynomial.eval₂ f x (p * Polynomial.X) = Polynomial.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) : Polynomial.eval₂ f x (Polynomial.X * p) = Polynomial.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) : Polynomial.eval₂ f x (p * Polynomial.C a) = Polynomial.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) : Polynomial.eval₂ f x ps.prod = (List.map (Polynomial.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) : (Polynomial.eval₂RingHom' f x hf) p = Polynomial.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) : 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} [CommSemiring 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} [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hq : Polynomial.eval₂ f x q = 0) : Polynomial.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) : ⇑(Polynomial.eval₂RingHom f x) = Polynomial.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 : ℕ) : Polynomial.eval₂ f x (p ^ n) = Polynomial.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 → Polynomial.eval₂ f x p ∣ Polynomial.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 : Polynomial.eval₂ f x p = 0) : Polynomial.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) : Polynomial.eval₂ f x l.prod = (List.map (Polynomial.eval₂ f x) l).prod

def Polynomial.eval {R : Type u} [Semiring R] : R → Polynomial R → R

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

Equations

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

theorem Polynomial.eval_eq_sum {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.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) : Polynomial.eval₂ f (f r) p = f (Polynomial.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) : Polynomial.eval₂ f 1 p = f (Polynomial.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 : ℕ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)

@[deprecated Polynomial.eval₂_at_natCast]

theorem Polynomial.eval₂_at_nat_cast {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)

Alias of Polynomial.eval₂_at_natCast.

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

@[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_natCast {R : Type u} [Semiring R] {x : R} {n : ℕ} : Polynomial.eval x ↑n = ↑n

@[deprecated Polynomial.eval_natCast]

theorem Polynomial.eval_nat_cast {R : Type u} [Semiring R] {x : R} {n : ℕ} : Polynomial.eval x ↑n = ↑n

Alias of Polynomial.eval_natCast.

@[simp]

theorem Polynomial.eval_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] (a : R) : Polynomial.eval a (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Polynomial.eval_X {R : Type u} [Semiring R] {x : R} : Polynomial.eval x Polynomial.X = x

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

theorem Polynomial.eval_zero {R : Type u} [Semiring R] {x : R} : Polynomial.eval x 0 = 0

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

theorem Polynomial.eval_one {R : Type u} [Semiring R] {x : R} : Polynomial.eval x 1 = 1

@[simp]

theorem Polynomial.eval_C_mul {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p

@[simp]

theorem Polynomial.eval_natCast_mul {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {n : ℕ} : Polynomial.eval x (↑n * p) = ↑n * Polynomial.eval x p

@[deprecated Polynomial.eval_natCast_mul]

theorem Polynomial.eval_nat_cast_mul {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {n : ℕ} : Polynomial.eval x (↑n * p) = ↑n * Polynomial.eval x p

Alias of Polynomial.eval_natCast_mul.

@[simp]

theorem Polynomial.eval_mul_X {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (p * Polynomial.X) = Polynomial.eval x p * x

@[simp]

theorem Polynomial.eval_mul_X_pow {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {k : ℕ} : Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k

theorem Polynomial.eval_sum {R : Type u} [Semiring R] (p : Polynomial R) (f : ℕ → R → Polynomial R) (x : R) : Polynomial.eval x (p.sum f) = p.sum fun (n : ℕ) (a : R) => Polynomial.eval x (f n a)

theorem Polynomial.eval_finset_sum {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (g : ι → Polynomial R) (x : R) : Polynomial.eval x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.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 ↔ Polynomial.eval a p = 0

theorem Polynomial.IsRoot.eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : R} (h : p.IsRoot x) : Polynomial.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) : ¬(Polynomial.C r).IsRoot a

theorem Polynomial.eval_surjective {R : Type u} [Semiring R] (x : R) : Function.Surjective (Polynomial.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) => Polynomial.C a * q ^ e

@[simp]

theorem Polynomial.comp_X {R : Type u} [Semiring R] {p : Polynomial R} : p.comp Polynomial.X = p

@[simp]

theorem Polynomial.X_comp {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.X.comp p = p

@[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.natCast_comp {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (↑n).comp p = ↑n

@[deprecated Polynomial.natCast_comp]

theorem Polynomial.nat_cast_comp {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (↑n).comp p = ↑n

Alias of Polynomial.natCast_comp.

@[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 = Polynomial.C (Polynomial.eval 0 p)

@[simp]

theorem Polynomial.zero_comp {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.comp 0 p = 0

@[simp]

theorem Polynomial.comp_one {R : Type u} [Semiring R] {p : Polynomial R} : p.comp 1 = Polynomial.C (Polynomial.eval 1 p)

@[simp]

theorem Polynomial.one_comp {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.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 : ℕ) : ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n

@[simp]

theorem Polynomial.mul_X_comp {R : Type u} [Semiring R] {p r : Polynomial R} : (p * Polynomial.X).comp r = p.comp r * r

@[simp]

theorem Polynomial.X_pow_comp {R : Type u} [Semiring R] {p : Polynomial R} {k : ℕ} : (Polynomial.X ^ k).comp p = p ^ k

@[simp]

theorem Polynomial.mul_X_pow_comp {R : Type u} [Semiring R] {p r : Polynomial R} {k : ℕ} : (p * Polynomial.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} : (Polynomial.C a * p).comp r = Polynomial.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

@[deprecated Polynomial.natCast_mul_comp]

theorem Polynomial.nat_cast_mul_comp {R : Type u} [Semiring R] {p r : Polynomial R} {n : ℕ} : (↑n * p).comp r = ↑n * p.comp r

Alias of Polynomial.natCast_mul_comp.

theorem Polynomial.mul_X_add_natCast_comp {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)

@[deprecated Polynomial.mul_X_add_natCast_comp]

theorem Polynomial.mul_X_add_nat_cast_comp {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X + ↑n)).comp q = p.comp q * (q + ↑n)

Alias of Polynomial.mul_X_add_natCast_comp.

@[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) : Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)

@[simp]

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

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

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) : ⇑(Polynomial.mapRingHom f) = Polynomial.map f

@[simp]

theorem Polynomial.map_natCast {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.map f ↑n = ↑n

@[deprecated map_natCast]

theorem Polynomial.map_nat_cast {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) : f ↑n = ↑n

Alias of map_natCast.

@[simp]

theorem Polynomial.map_ofNat {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] : Polynomial.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 → Polynomial.map f x ∣ Polynomial.map f y

theorem Polynomial.mapRingHom_comp_C {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : (Polynomial.mapRingHom f).comp Polynomial.C = Polynomial.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} : Polynomial.eval₂ f x p = Polynomial.eval x (Polynomial.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)) : 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.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

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

@[simp]

theorem Polynomial.eval_mul {R : Type u} [CommSemiring R] {p q : Polynomial R} {x : R} : Polynomial.eval x (p * q) = Polynomial.eval x p * Polynomial.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) : ⇑(Polynomial.evalRingHom r) = Polynomial.eval r

@[simp]

theorem Polynomial.eval_pow {R : Type u} [CommSemiring R] {p : Polynomial R} {x : R} (n : ℕ) : Polynomial.eval x (p ^ n) = Polynomial.eval x p ^ n

@[simp]

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

theorem Polynomial.eval_list_prod {R : Type u} [CommSemiring R] (l : List (Polynomial R)) (x : R) : Polynomial.eval x l.prod = (List.map (Polynomial.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) : Polynomial.eval x s.prod = (Multiset.map (Polynomial.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) : Polynomial.eval x (∏ j ∈ s, p j) = ∏ j ∈ s, Polynomial.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} [CommRing 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 → Polynomial.eval x p ∣ Polynomial.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 → Polynomial.eval x p = 0 → Polynomial.eval x q = 0

@[simp]

theorem Polynomial.eval_geom_sum {R : Type u_1} [CommSemiring R] {n : ℕ} {x : R} : Polynomial.eval x (∑ i ∈ Finset.range n, Polynomial.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)) : Polynomial.map f m.prod = (Multiset.map (Polynomial.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 ι) : Polynomial.map f (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.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) : 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} [Ring S] (f : R →+* S) : Polynomial.map f (-p) = -Polynomial.map f p

@[simp]

theorem Polynomial.map_intCast {R : Type u} [Ring R] {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.map f ↑n = ↑n

@[deprecated map_intCast]

theorem Polynomial.map_int_cast {F : Type u_1} {α : Type u_3} {β : Type u_4} [NonAssocRing α] [NonAssocRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f ↑n = ↑n

Alias of map_intCast.

@[simp]

theorem Polynomial.eval_intCast {R : Type u} [Ring R] {n : ℤ} {x : R} : Polynomial.eval x ↑n = ↑n

@[deprecated Polynomial.eval_intCast]

theorem Polynomial.eval_int_cast {R : Type u} [Ring R] {n : ℤ} {x : R} : Polynomial.eval x ↑n = ↑n

Alias of Polynomial.eval_intCast.

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

@[deprecated Polynomial.intCast_comp]

theorem Polynomial.cast_int_comp {R : Type u} [Ring R] {p : Polynomial R} (i : ℤ) : (↑i).comp p = ↑i

Alias of Polynomial.intCast_comp.

@[simp]

theorem Polynomial.eval₂_at_intCast {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)

@[deprecated Polynomial.eval₂_at_intCast]

theorem Polynomial.eval₂_at_int_cast {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)

Alias of Polynomial.eval₂_at_intCast.

theorem Polynomial.mul_X_sub_intCast_comp {R : Type u} [Ring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)

@[deprecated Polynomial.mul_X_sub_intCast_comp]

theorem Polynomial.mul_X_sub_int_cast_comp {R : Type u} [Ring R] {p q : Polynomial R} {n : ℕ} : (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)

Alias of Polynomial.mul_X_sub_intCast_comp.