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.

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

@[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₂ = Polynomial.wrapped✝.1

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 : R →+* S} {g : R →+* S} {s : S} {t : S} {φ : Polynomial R} {ψ : Polynomial R} : f = g → s = t → φ = ψ → Polynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ

@[simp]

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

@[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 : Polynomial R} {q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (p + q) = Polynomial.eval₂ f x p + Polynomial.eval₂ f x q

@[simp]

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

@[simp]

theorem Polynomial.eval₂_smul {R : Type u} {S : Type v} [Semiring R] [Semiring S] (g : R →+* S) (p : Polynomial R) (x : S) {s : R} : Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p

@[simp]

theorem Polynomial.eval₂_C_X {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.eval₂ Polynomial.C Polynomial.X p = p

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

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₂_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 : Polynomial R} {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

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

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' := ⋯ }

We next prove that eval₂ is multiplicative as long as target ring is commutative (even if the source ring is not).

theorem Polynomial.eval₂_eq_sum_range {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i

theorem Polynomial.eval₂_eq_sum_range' {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i

@[simp]

theorem Polynomial.eval₂_mul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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

theorem Polynomial.eval_eq_sum_range {R : Type u} [Semiring R] {p : Polynomial R} (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i

theorem Polynomial.eval_eq_sum_range' {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i

@[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 : Polynomial R} {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_smul {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (x : R) : Polynomial.eval x (s • p) = s • Polynomial.eval x p

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

theorem Polynomial.eval_monomial_one_add_sub {S : Type v} [CommRing S] (d : ℕ) (y : S) : Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

A reformulation of the expansion of (1 + y)^d: $$(d+1)(1+y{)}^d-(d+1)y^d=\sum _{i=0}^d(\genfrac{}{}{0ex}{}{d+1}{i})\cdot i\cdot y^{i-1}.$$

@[simp]

theorem Polynomial.leval_apply {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : (Polynomial.leval r) f = Polynomial.eval r f

def Polynomial.leval {R : Type u_1} [Semiring R] (r : R) : Polynomial R →ₗ[R] R

Polynomial.eval as linear map

Equations

• Polynomial.leval r = { toFun := fun (f : Polynomial R) => Polynomial.eval r f, map_add' := ⋯, map_smul' := ⋯ }

@[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.coeff_zero_eq_eval_zero {R : Type u} [Semiring R] (p : Polynomial R) : p.coeff 0 = Polynomial.eval 0 p

theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.coeff 0 = 0) : p.IsRoot 0

theorem Polynomial.IsRoot.dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} {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 : 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 : Polynomial R) (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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R) (q : Polynomial R) (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 : Polynomial R) (q : Polynomial R) (n : ℕ) : (p ^ n).comp q = p.comp q ^ n

@[simp]

theorem Polynomial.smul_comp {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (q : Polynomial R) : (s • p).comp q = s • p.comp q

theorem Polynomial.comp_assoc {R : Type u_1} [CommSemiring R] (φ : Polynomial R) (ψ : Polynomial R) (χ : Polynomial R) : (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

theorem Polynomial.coeff_comp_degree_mul_degree {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hqd0 : q.natDegree ≠ 0) : (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

@[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 : Polynomial R} {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 : Polynomial R} {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_smul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (r : R) : Polynomial.map f (r • p) = f r • Polynomial.map f p

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 : Polynomial R} {y : Polynomial R} : x ∣ y → Polynomial.map f x ∣ Polynomial.map f y

@[simp]

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

@[simp]

theorem Polynomial.mapEquiv_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial R) : (Polynomial.mapEquiv e) a = Polynomial.map (↑e) a

@[simp]

theorem Polynomial.mapEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial S) : (Polynomial.mapEquiv e).symm a = Polynomial.map (↑e.symm) a

def Polynomial.mapEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) : Polynomial R ≃+* Polynomial S

If R and S are isomorphic, then so are their polynomial rings.

Equations

• Polynomial.mapEquiv e = RingEquiv.ofHomInv (Polynomial.mapRingHom ↑e) (Polynomial.mapRingHom ↑e.symm) ⋯ ⋯

theorem Polynomial.map_map {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] (f : R →+* S) [Semiring T] (g : S →+* T) (p : Polynomial R) : Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp f) p

@[simp]

theorem Polynomial.map_id {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.map (RingHom.id R) p = p

def Polynomial.piEquiv {ι : Type u_2} [Finite ι] (R : ι → Type u_1) [(i : ι) → Semiring (R i)] : Polynomial ((i : ι) → R i) ≃+* ((i : ι) → Polynomial (R i))

The polynomial ring over a finite product of rings is isomorphic to the product of polynomial rings over individual rings.

Equations

• Polynomial.piEquiv R = RingEquiv.ofBijective (Pi.ringHom fun (i : ι) => Polynomial.mapRingHom (Pi.evalRingHom R i)) ⋯

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

theorem Polynomial.map_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (Polynomial.map f)

theorem Polynomial.map_surjective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : Function.Surjective (Polynomial.map f)

theorem Polynomial.degree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (Polynomial.map f p).degree ≤ p.degree

theorem Polynomial.natDegree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (Polynomial.map f p).natDegree ≤ p.natDegree

theorem Polynomial.map_eq_zero_iff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) : Polynomial.map f p = 0 ↔ p = 0

theorem Polynomial.map_ne_zero_iff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) : Polynomial.map f p ≠ 0 ↔ p ≠ 0

theorem Polynomial.map_monic_eq_zero_iff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hp : p.Monic) : Polynomial.map f p = 0 ↔ ∀ (x : R), f x = 0

theorem Polynomial.map_monic_ne_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hp : p.Monic) [Nontrivial S] : Polynomial.map f p ≠ 0

theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).degree = p.degree

theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).natDegree = p.natDegree

theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff

@[simp]

theorem Polynomial.mapRingHom_id {R : Type u} [Semiring R] : Polynomial.mapRingHom (RingHom.id R) = RingHom.id (Polynomial R)

@[simp]

theorem Polynomial.mapRingHom_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : S →+* T) (g : R →+* S) : (Polynomial.mapRingHom f).comp (Polynomial.mapRingHom g) = Polynomial.mapRingHom (f.comp g)

theorem Polynomial.map_list_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (L : List (Polynomial R)) : Polynomial.map f L.prod = (List.map (Polynomial.map f) L).prod

@[simp]

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

theorem Polynomial.mem_map_rangeS {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial S} : p ∈ (Polynomial.mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

theorem Polynomial.mem_map_range {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {p : Polynomial S} : p ∈ (Polynomial.mapRingHom f).range ↔ ∀ (n : ℕ), p.coeff n ∈ f.range

theorem Polynomial.eval₂_map {R : Type u} {S : Type v} {T : Type w} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) [Semiring T] (g : S →+* T) (x : T) : Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.eval₂ (g.comp f) x p

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

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 : Polynomial R) (q : Polynomial R) : Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)

@[simp]

theorem Polynomial.eval_zero_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : Polynomial.eval 0 (Polynomial.map f p) = f (Polynomial.eval 0 p)

@[simp]

theorem Polynomial.eval_one_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : Polynomial.eval 1 (Polynomial.map f p) = f (Polynomial.eval 1 p)

@[simp]

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

@[deprecated Polynomial.eval_natCast_map]

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

Alias of Polynomial.eval_natCast_map.

@[simp]

theorem Polynomial.eval_intCast_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (p : Polynomial R) (i : ℤ) : Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)

@[deprecated Polynomial.eval_intCast_map]

theorem Polynomial.eval_int_cast_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (p : Polynomial R) (i : ℤ) : Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)

Alias of Polynomial.eval_intCast_map.

we have made eval₂ irreducible from the start.

Perhaps we can make also eval, comp, and map irreducible too?

theorem Polynomial.hom_eval₂ {R : Type u} {S : Type v} {T : Type w} [Semiring R] (p : Polynomial R) [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) (x : S) : g (Polynomial.eval₂ f x p) = Polynomial.eval₂ (g.comp f) (g x) p

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

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

@[simp]

theorem Polynomial.iterate_comp_eval₂ {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [CommSemiring S] (f : R →+* S) (k : ℕ) (t : S) : Polynomial.eval₂ f t (p.comp^[k] q) = (fun (x : S) => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)

@[simp]

theorem Polynomial.eval₂_mul' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) (q : Polynomial R) : Polynomial.eval₂ (algebraMap R S) x (p * q) = Polynomial.eval₂ (algebraMap R S) x p * Polynomial.eval₂ (algebraMap R S) x q

@[simp]

theorem Polynomial.eval₂_pow' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) (n : ℕ) : Polynomial.eval₂ (algebraMap R S) x (p ^ n) = Polynomial.eval₂ (algebraMap R S) x p ^ n

@[simp]

theorem Polynomial.eval₂_comp' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) (q : Polynomial R) : Polynomial.eval₂ (algebraMap R S) x (p.comp q) = Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p

@[simp]

theorem Polynomial.eval_mul {R : Type u} [CommSemiring R] {p : Polynomial R} {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

theorem Polynomial.evalRingHom_zero : Polynomial.evalRingHom 0 = Polynomial.constantCoeff

@[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 : Polynomial R} {q : Polynomial R} {x : R} : Polynomial.eval x (p.comp q) = Polynomial.eval (Polynomial.eval x q) p

@[simp]

theorem Polynomial.iterate_comp_eval {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} (k : ℕ) (t : R) : Polynomial.eval t (p.comp^[k] q) = (fun (x : R) => Polynomial.eval x p)^[k] (Polynomial.eval t q)

theorem Polynomial.isRoot_comp {R : Type u_1} [CommSemiring R] {p : Polynomial R} {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 : Polynomial R) (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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} [NoZeroDivisors R] (h : (p * q).IsRoot a) : p.IsRoot a ∨ q.IsRoot a

theorem Polynomial.support_map_subset {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (Polynomial.map f p).support ⊆ p.support

theorem Polynomial.support_map_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) {f : R →+* S} (hf : Function.Injective ⇑f) : (Polynomial.map f p).support = p.support

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)

theorem Polynomial.IsRoot.map {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R} (h : p.IsRoot x) : (Polynomial.map f p).IsRoot (f x)

theorem Polynomial.IsRoot.of_map {S : Type v} [CommSemiring S] {R : Type u_1} [CommRing R] {f : R →+* S} {x : R} {p : Polynomial R} (h : (Polynomial.map f p).IsRoot (f x)) (hf : Function.Injective ⇑f) : p.IsRoot x

theorem Polynomial.isRoot_map_iff {S : Type v} [CommSemiring S] {R : Type u_1} [CommRing R] {f : R →+* S} {x : R} {p : Polynomial R} (hf : Function.Injective ⇑f) : (Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x

@[simp]

theorem Polynomial.map_sub {R : Type u} [Ring R] {p : Polynomial R} {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 : Polynomial R} {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 : Polynomial R) (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 : R} {b : R} [Ring R] : (Polynomial.X - Polynomial.C a).IsRoot b ↔ a = b

@[simp]

theorem Polynomial.neg_comp {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} : (-p).comp q = -p.comp q

@[simp]

theorem Polynomial.sub_comp {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {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 : Polynomial R} {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 : Polynomial R} {q : Polynomial R} {n : ℕ} : (p * (Polynomial.X - ↑n)).comp q = p.comp q * (q - ↑n)

Alias of Polynomial.mul_X_sub_intCast_comp.

theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit f.leadingCoeff) (H : IsUnit (Polynomial.map φ f)) : IsUnit f

theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (φ : R →+* S) (f : Polynomial R) (h_mon : f.Monic) (h_irr : Irreducible (Polynomial.map φ f)) : Irreducible f

A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S.

A special case of this lemma is that a polynomial over ℤ is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.