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 = Polynomial.sum p 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 = Polynomial.sum p 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 (Polynomial.coeff p 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₂_bit0 {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (bit0 p) = bit0 (Polynomial.eval₂ f x p)

@[simp]

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

@[simp]

theorem Polynomial.eval₂_smul {R : Type u} {S : Type v} [Semiring R] [Semiring S] (g : R →+* S) (p : Polynomial R) (x : S) {s : R} : 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 = { toZeroHom := { toFun := Polynomial.eval₂ f x, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

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

@[simp]

theorem Polynomial.eval₂_ofNat {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] (n : ℕ) [Nat.AtLeastTwo n] (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 (Polynomial.sum p g) = Polynomial.sum p 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 (List.sum l) = List.sum (List.map (Polynomial.eval₂ f x) l)

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 (Multiset.sum s) = Multiset.sum (Multiset.map (Polynomial.eval₂ f x) s)

theorem Polynomial.eval₂_finset_sum {R : Type u} {S : Type v} {ι : Type y} [Semiring R] [Semiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (Finset.sum s fun (i : ι) => g i) = Finset.sum s fun (i : ι) => 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 (Polynomial.coeff q 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 (Polynomial.coeff p k)) x) : Polynomial.eval₂ f x (List.prod ps) = List.prod (List.map (Polynomial.eval₂ f x) ps)

@[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 = { toMonoidHom := { toOneHom := { 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 = Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun (i : ℕ) => f (Polynomial.coeff p 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 : Polynomial.natDegree p < n) (x : S) : Polynomial.eval₂ f x p = Finset.sum (Finset.range n) fun (i : ℕ) => f (Polynomial.coeff p 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

• One or more equations did not get rendered due to their size.

@[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 (List.prod l) = List.prod (List.map (Polynomial.eval₂ f x) l)

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 = Polynomial.sum p 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 = Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun (i : ℕ) => Polynomial.coeff p i * x ^ i

theorem Polynomial.eval_eq_sum_range' {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : Polynomial.natDegree p < n) (x : R) : Polynomial.eval x p = Finset.sum (Finset.range n) fun (i : ℕ) => Polynomial.coeff p 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_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)

@[simp]

theorem Polynomial.eval₂_at_ofNat {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ℕ) [Nat.AtLeastTwo n] : 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_nat_cast {R : Type u} [Semiring R] {x : R} {n : ℕ} : Polynomial.eval x ↑n = ↑n

@[simp]

theorem Polynomial.eval_ofNat {R : Type u} [Semiring R] (n : ℕ) [Nat.AtLeastTwo n] (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_bit0 {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (bit0 p) = bit0 (Polynomial.eval x p)

@[simp]

theorem Polynomial.eval_bit1 {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x (bit1 p) = bit1 (Polynomial.eval x p)

@[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)) = Finset.sum (Finset.range (d + 1)) fun (x_1 : ℕ) => ↑(Nat.choose (d + 1) 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 {d + 1 \choose 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 = { toAddHom := { toFun := fun (f : Polynomial R) => Polynomial.eval r f, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

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

@[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 (Polynomial.sum p f) = Polynomial.sum p 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 (Finset.sum s fun (i : ι) => g i) = Finset.sum s fun (i : ι) => 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

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

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

Equations

• Polynomial.IsRoot.decidable = id inferInstance

@[simp]

theorem Polynomial.IsRoot.def {R : Type u} {a : R} [Semiring R] {p : Polynomial R} : Polynomial.IsRoot p a ↔ Polynomial.eval a p = 0

theorem Polynomial.IsRoot.eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : R} (h : Polynomial.IsRoot p x) : Polynomial.eval x p = 0

theorem Polynomial.coeff_zero_eq_eval_zero {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.coeff p 0 = Polynomial.eval 0 p

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

theorem Polynomial.IsRoot.dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {x : R} (h : Polynomial.IsRoot p x) (hpq : p ∣ q) : Polynomial.IsRoot q x

theorem Polynomial.not_isRoot_C {R : Type u} [Semiring R] (r : R) (a : R) (hr : r ≠ 0) : ¬Polynomial.IsRoot (Polynomial.C r) 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

• Polynomial.comp p q = Polynomial.eval₂ Polynomial.C q p

theorem Polynomial.comp_eq_sum_left {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} : Polynomial.comp p q = Polynomial.sum p fun (e : ℕ) (a : R) => Polynomial.C a * q ^ e

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.ofNat_comp {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) [Nat.AtLeastTwo n] : Polynomial.comp (OfNat.ofNat n) p = ↑n

@[simp]

theorem Polynomial.comp_zero {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.comp p 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} : Polynomial.comp p 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} : Polynomial.comp (p + q) r = Polynomial.comp p r + Polynomial.comp q r

@[simp]

theorem Polynomial.monomial_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ℕ) : Polynomial.comp ((Polynomial.monomial n) a) p = Polynomial.C a * p ^ n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.C_mul_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {r : Polynomial R} : Polynomial.comp (Polynomial.C a * p) r = Polynomial.C a * Polynomial.comp p r

@[simp]

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

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

@[simp]

theorem Polynomial.mul_comp {R : Type u_1} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (r : Polynomial R) : Polynomial.comp (p * q) r = Polynomial.comp p r * Polynomial.comp q r

@[simp]

theorem Polynomial.pow_comp {R : Type u_1} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (n : ℕ) : Polynomial.comp (p ^ n) q = Polynomial.comp p q ^ n

@[simp]

theorem Polynomial.bit0_comp {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} : Polynomial.comp (bit0 p) q = bit0 (Polynomial.comp p q)

@[simp]

theorem Polynomial.bit1_comp {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} : Polynomial.comp (bit1 p) q = bit1 (Polynomial.comp p q)

@[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) : Polynomial.comp (s • p) q = s • Polynomial.comp p q

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

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

@[simp]

theorem Polynomial.sum_comp {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R) : Polynomial.comp (Finset.sum s fun (i : ι) => p i) q = Finset.sum s fun (i : ι) => Polynomial.comp (p i) 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₂ (RingHom.comp Polynomial.C 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 = { toMonoidHom := { toOneHom := { 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_nat_cast {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.map f ↑n = ↑n

@[simp]

theorem Polynomial.map_ofNat {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) [Nat.AtLeastTwo n] : Polynomial.map f (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

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

@[simp]

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

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.coeff (Polynomial.map f p) n = f (Polynomial.coeff p n)

@[simp]

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

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

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 ↑(RingEquiv.symm e)) ⋯ ⋯

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 (RingHom.comp g 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.degree (Polynomial.map f p) ≤ Polynomial.degree p

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

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 : Polynomial.Monic p) : 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 : Polynomial.Monic p) [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 (Polynomial.leadingCoeff p) ≠ 0) : Polynomial.degree (Polynomial.map f p) = Polynomial.degree p

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 (Polynomial.leadingCoeff p) ≠ 0) : Polynomial.natDegree (Polynomial.map f p) = Polynomial.natDegree p

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 (Polynomial.leadingCoeff p) ≠ 0) : Polynomial.leadingCoeff (Polynomial.map f p) = f (Polynomial.leadingCoeff p)

@[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) : RingHom.comp (Polynomial.mapRingHom f) (Polynomial.mapRingHom g) = Polynomial.mapRingHom (RingHom.comp f 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 (List.prod L) = List.prod (List.map (Polynomial.map f) L)

@[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 ∈ RingHom.rangeS (Polynomial.mapRingHom f) ↔ ∀ (n : ℕ), Polynomial.coeff p n ∈ RingHom.rangeS f

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

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₂ (RingHom.comp g 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 (Finset.sum s fun (i : ι) => g i) = Finset.sum s fun (i : ι) => 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 (Polynomial.comp p q) = Polynomial.comp (Polynomial.map f p) (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_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)

@[simp]

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)

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₂ (RingHom.comp g 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 (Polynomial.comp p 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 ((Polynomial.comp p)^[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 (Polynomial.comp p 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 (Polynomial.comp p 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 ((Polynomial.comp p)^[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} : Polynomial.IsRoot (Polynomial.comp p q) r ↔ Polynomial.IsRoot p (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) : ⇑(Polynomial.compRingHom q) = fun (p : Polynomial R) => Polynomial.comp p q

theorem Polynomial.coe_compRingHom_apply {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) : (Polynomial.compRingHom q) p = Polynomial.comp p q

theorem Polynomial.root_mul_left_of_isRoot {R : Type u} {a : R} [CommSemiring R] (p : Polynomial R) {q : Polynomial R} : Polynomial.IsRoot q a → Polynomial.IsRoot (p * q) a

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

theorem Polynomial.eval₂_finset_prod {R : Type u} {S : Type v} {ι : Type y} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (Finset.prod s fun (i : ι) => g i) = Finset.prod s fun (i : ι) => 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 (List.prod l) = List.prod (List.map (Polynomial.eval x) l)

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 (Multiset.prod s) = Multiset.prod (Multiset.map (Polynomial.eval x) s)

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 (Finset.prod s fun (j : ι) => p j) = Finset.prod s fun (j : ι) => 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) : Polynomial.comp (List.prod l) q = List.prod (List.map (fun (p : Polynomial R) => Polynomial.comp p q) l)

theorem Polynomial.multiset_prod_comp {R : Type u} [CommSemiring R] (s : Multiset (Polynomial R)) (q : Polynomial R) : Polynomial.comp (Multiset.prod s) q = Multiset.prod (Multiset.map (fun (p : Polynomial R) => Polynomial.comp p q) s)

theorem Polynomial.prod_comp {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R) : Polynomial.comp (Finset.prod s fun (j : ι) => p j) q = Finset.prod s fun (j : ι) => Polynomial.comp (p j) q

theorem Polynomial.isRoot_prod {R : Type u_2} [CommRing R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R) : Polynomial.IsRoot (Finset.prod s fun (j : ι) => p j) x ↔ ∃ i ∈ s, Polynomial.IsRoot (p i) 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 (Finset.sum (Finset.range n) fun (i : ℕ) => Polynomial.X ^ i) = Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i

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

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.support (Polynomial.map f p) = Polynomial.support p

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 (Multiset.prod m) = Multiset.prod (Multiset.map (Polynomial.map f) m)

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 (Finset.prod s fun (i : ι) => g i) = Finset.prod s fun (i : ι) => 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 : Polynomial.IsRoot p x) : Polynomial.IsRoot (Polynomial.map f p) (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.IsRoot (Polynomial.map f p) (f x)) (hf : Function.Injective ⇑f) : Polynomial.IsRoot p 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.IsRoot (Polynomial.map f p) (f x) ↔ Polynomial.IsRoot p 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_int_cast {R : Type u} [Ring R] {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.map f ↑n = ↑n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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)

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