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} [] [] (f : R →+* S) (x : S) (p : ) :
= Polynomial.sum p fun (e : ) (a : R) => f a * x ^ e
@[irreducible]
def Polynomial.eval₂ {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) (x : S) (p : ) :
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
Instances For
theorem Polynomial.eval₂_eq_sum {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} {x : S} :
= Polynomial.sum p fun (e : ) (a : R) => f a * x ^ e
theorem Polynomial.eval₂_congr {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} {g : R →+* S} {s : S} {t : S} {φ : } {ψ : } :
f = gs = tφ = ψ =
@[simp]
theorem Polynomial.eval₂_at_zero {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) :
= f ()
@[simp]
theorem Polynomial.eval₂_zero {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) :
= 0
@[simp]
theorem Polynomial.eval₂_C {R : Type u} {S : Type v} {a : R} [] [] (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} [] [] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x Polynomial.X = x
@[simp]
theorem Polynomial.eval₂_monomial {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) {n : } {r : R} :
Polynomial.eval₂ f x ( r) = f r * x ^ n
@[simp]
theorem Polynomial.eval₂_X_pow {R : Type u} {S : Type v} [] [] (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} [] {p : } {q : } [] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x (p + q) = +
@[simp]
theorem Polynomial.eval₂_one {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) :
= 1
@[simp]
theorem Polynomial.eval₂_bit0 {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) :
@[simp]
theorem Polynomial.eval₂_bit1 {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) :
@[simp]
theorem Polynomial.eval₂_smul {R : Type u} {S : Type v} [] [] (g : R →+* S) (p : ) (x : S) {s : R} :
Polynomial.eval₂ g x (s p) = g s *
@[simp]
theorem Polynomial.eval₂_C_X {R : Type u} [] {p : } :
Polynomial.eval₂ Polynomial.C Polynomial.X p = p
@[simp]
theorem Polynomial.eval₂AddMonoidHom_apply {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) (p : ) :
p =
def Polynomial.eval₂AddMonoidHom {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) :
→+ 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.eval₂_nat_cast {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) (n : ) :
Polynomial.eval₂ f x n = n
@[simp]
theorem Polynomial.eval₂_ofNat {R : Type u} [] {S : Type u_1} [] (n : ) [] (f : R →+* S) (a : S) :
=
theorem Polynomial.eval₂_sum {R : Type u} {S : Type v} {T : Type w} [] [] (f : R →+* S) [] (p : ) (g : T) (x : S) :
Polynomial.eval₂ f x () = 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} [] [] (f : R →+* S) (l : List ()) (x : S) :
theorem Polynomial.eval₂_multiset_sum {R : Type u} {S : Type v} [] [] (f : R →+* S) (s : ) (x : S) :
theorem Polynomial.eval₂_finset_sum {R : Type u} {S : Type v} {ι : Type y} [] [] (f : R →+* S) (s : ) (g : ι) (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} [] [] {f : R →+* S} {x : S} {p : } :
Polynomial.eval₂ f x { toFinsupp := p } = (AddMonoidAlgebra.liftNC f (() x)) p
theorem Polynomial.eval₂_mul_noncomm {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) (x : S) (hf : ∀ (k : ), Commute (f ()) x) :
Polynomial.eval₂ f x (p * q) = *
@[simp]
theorem Polynomial.eval₂_mul_X {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x (p * Polynomial.X) = * x
@[simp]
theorem Polynomial.eval₂_X_mul {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x (Polynomial.X * p) = * x
theorem Polynomial.eval₂_mul_C' {R : Type u} {S : Type v} {a : R} [] {p : } [] (f : R →+* S) (x : S) (h : Commute (f a) x) :
Polynomial.eval₂ f x (p * Polynomial.C a) = * f a
theorem Polynomial.eval₂_list_prod_noncomm {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) (ps : List ()) (hf : pps, ∀ (k : ), Commute (f ()) x) :
@[simp]
theorem Polynomial.eval₂RingHom'_apply {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) (p : ) :
() p =
def Polynomial.eval₂RingHom' {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) :

eval₂ as a RingHom for noncommutative rings

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

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} [] {p : } [] (f : R →+* S) (x : S) :
= Finset.sum () fun (i : ) => f () * x ^ i
theorem Polynomial.eval₂_eq_sum_range' {R : Type u} {S : Type v} [] [] (f : R →+* S) {p : } {n : } (hn : ) (x : S) :
= Finset.sum () fun (i : ) => f () * x ^ i
@[simp]
theorem Polynomial.eval₂_mul {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x (p * q) = *
theorem Polynomial.eval₂_mul_eq_zero_of_left {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) (q : ) (hp : = 0) :
Polynomial.eval₂ f x (p * q) = 0
theorem Polynomial.eval₂_mul_eq_zero_of_right {R : Type u} {S : Type v} [] {q : } [] (f : R →+* S) (x : S) (p : ) (hq : = 0) :
Polynomial.eval₂ f x (p * q) = 0
def Polynomial.eval₂RingHom {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) :

eval₂ as a RingHom

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.coe_eval₂RingHom {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : S) :
() =
theorem Polynomial.eval₂_pow {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) (n : ) :
Polynomial.eval₂ f x (p ^ n) = ^ n
theorem Polynomial.eval₂_dvd {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) (x : S) :
p q
theorem Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) (x : S) (h : p q) (h0 : = 0) :
= 0
theorem Polynomial.eval₂_list_prod {R : Type u} {S : Type v} [] [] (f : R →+* S) (l : List ()) (x : S) :
def Polynomial.eval {R : Type u} [] :
RR

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

Equations
• Polynomial.eval =
Instances For
theorem Polynomial.eval_eq_sum {R : Type u} [] {p : } {x : R} :
= Polynomial.sum p fun (e : ) (a : R) => a * x ^ e
theorem Polynomial.eval_eq_sum_range {R : Type u} [] {p : } (x : R) :
= Finset.sum () fun (i : ) => * x ^ i
theorem Polynomial.eval_eq_sum_range' {R : Type u} [] {p : } {n : } (hn : ) (x : R) :
= Finset.sum () fun (i : ) => * x ^ i
@[simp]
theorem Polynomial.eval₂_at_apply {R : Type u} [] {p : } {S : Type u_1} [] (f : R →+* S) (r : R) :
Polynomial.eval₂ f (f r) p = f ()
@[simp]
theorem Polynomial.eval₂_at_one {R : Type u} [] {p : } {S : Type u_1} [] (f : R →+* S) :
= f ()
@[simp]
theorem Polynomial.eval₂_at_nat_cast {R : Type u} [] {p : } {S : Type u_1} [] (f : R →+* S) (n : ) :
Polynomial.eval₂ f (n) p = f (Polynomial.eval (n) p)
@[simp]
theorem Polynomial.eval₂_at_ofNat {R : Type u} [] {p : } {S : Type u_1} [] (f : R →+* S) (n : ) [] :
= f ()
@[simp]
theorem Polynomial.eval_C {R : Type u} {a : R} [] {x : R} :
Polynomial.eval x (Polynomial.C a) = a
@[simp]
theorem Polynomial.eval_nat_cast {R : Type u} [] {x : R} {n : } :
= n
@[simp]
theorem Polynomial.eval_ofNat {R : Type u} [] (n : ) [] (a : R) :
@[simp]
theorem Polynomial.eval_X {R : Type u} [] {x : R} :
Polynomial.eval x Polynomial.X = x
@[simp]
theorem Polynomial.eval_monomial {R : Type u} [] {x : R} {n : } {a : R} :
Polynomial.eval x ( a) = a * x ^ n
@[simp]
theorem Polynomial.eval_zero {R : Type u} [] {x : R} :
= 0
@[simp]
theorem Polynomial.eval_add {R : Type u} [] {p : } {q : } {x : R} :
Polynomial.eval x (p + q) = +
@[simp]
theorem Polynomial.eval_one {R : Type u} [] {x : R} :
= 1
@[simp]
theorem Polynomial.eval_bit0 {R : Type u} [] {p : } {x : R} :
@[simp]
theorem Polynomial.eval_bit1 {R : Type u} [] {p : } {x : R} :
@[simp]
theorem Polynomial.eval_smul {R : Type u} {S : Type v} [] [] [] [] (s : S) (p : ) (x : R) :
@[simp]
theorem Polynomial.eval_C_mul {R : Type u} {a : R} [] {p : } {x : R} :
Polynomial.eval x (Polynomial.C a * p) = a *
theorem Polynomial.eval_monomial_one_add_sub {S : Type v} [] (d : ) (y : S) :
Polynomial.eval (1 + y) ( (d + 1)) - Polynomial.eval y ( (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} [] (r : R) (f : ) :
() f =
def Polynomial.leval {R : Type u_1} [] (r : R) :

Polynomial.eval as linear map

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.eval_nat_cast_mul {R : Type u} [] {p : } {x : R} {n : } :
Polynomial.eval x (n * p) = n *
@[simp]
theorem Polynomial.eval_mul_X {R : Type u} [] {p : } {x : R} :
Polynomial.eval x (p * Polynomial.X) = * x
@[simp]
theorem Polynomial.eval_mul_X_pow {R : Type u} [] {p : } {x : R} {k : } :
Polynomial.eval x (p * Polynomial.X ^ k) = * x ^ k
theorem Polynomial.eval_sum {R : Type u} [] (p : ) (f : R) (x : R) :
= Polynomial.sum p fun (n : ) (a : R) => Polynomial.eval x (f n a)
theorem Polynomial.eval_finset_sum {R : Type u} {ι : Type y} [] (s : ) (g : ι) (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} [] (p : ) (a : R) :

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

Equations
Instances For
instance Polynomial.IsRoot.decidable {R : Type u} {a : R} [] {p : } [] :
Equations
• Polynomial.IsRoot.decidable = id inferInstance
@[simp]
theorem Polynomial.IsRoot.def {R : Type u} {a : R} [] {p : } :
= 0
theorem Polynomial.IsRoot.eq_zero {R : Type u} [] {p : } {x : R} (h : ) :
= 0
theorem Polynomial.coeff_zero_eq_eval_zero {R : Type u} [] (p : ) :
=
theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero {R : Type u} [] {p : } (hp : = 0) :
theorem Polynomial.IsRoot.dvd {R : Type u_1} [] {p : } {q : } {x : R} (h : ) (hpq : p q) :
theorem Polynomial.not_isRoot_C {R : Type u} [] (r : R) (a : R) (hr : r 0) :
¬Polynomial.IsRoot (Polynomial.C r) a
theorem Polynomial.eval_surjective {R : Type u} [] (x : R) :
def Polynomial.comp {R : Type u} [] (p : ) (q : ) :

The composition of polynomials as a polynomial.

Equations
Instances For
theorem Polynomial.comp_eq_sum_left {R : Type u} [] {p : } {q : } :
= Polynomial.sum p fun (e : ) (a : R) => Polynomial.C a * q ^ e
@[simp]
theorem Polynomial.comp_X {R : Type u} [] {p : } :
Polynomial.comp p Polynomial.X = p
@[simp]
theorem Polynomial.X_comp {R : Type u} [] {p : } :
Polynomial.comp Polynomial.X p = p
@[simp]
theorem Polynomial.comp_C {R : Type u} {a : R} [] {p : } :
Polynomial.comp p (Polynomial.C a) = Polynomial.C ()
@[simp]
theorem Polynomial.C_comp {R : Type u} {a : R} [] {p : } :
Polynomial.comp (Polynomial.C a) p = Polynomial.C a
@[simp]
theorem Polynomial.nat_cast_comp {R : Type u} [] {p : } {n : } :
Polynomial.comp (n) p = n
@[simp]
theorem Polynomial.ofNat_comp {R : Type u} [] {p : } (n : ) [] :
= n
@[simp]
theorem Polynomial.comp_zero {R : Type u} [] {p : } :
= Polynomial.C ()
@[simp]
theorem Polynomial.zero_comp {R : Type u} [] {p : } :
= 0
@[simp]
theorem Polynomial.comp_one {R : Type u} [] {p : } :
= Polynomial.C ()
@[simp]
theorem Polynomial.one_comp {R : Type u} [] {p : } :
= 1
@[simp]
theorem Polynomial.add_comp {R : Type u} [] {p : } {q : } {r : } :
Polynomial.comp (p + q) r = +
@[simp]
theorem Polynomial.monomial_comp {R : Type u} {a : R} [] {p : } (n : ) :
Polynomial.comp ( a) p = Polynomial.C a * p ^ n
@[simp]
theorem Polynomial.mul_X_comp {R : Type u} [] {p : } {r : } :
Polynomial.comp (p * Polynomial.X) r = * r
@[simp]
theorem Polynomial.X_pow_comp {R : Type u} [] {p : } {k : } :
Polynomial.comp (Polynomial.X ^ k) p = p ^ k
@[simp]
theorem Polynomial.mul_X_pow_comp {R : Type u} [] {p : } {r : } {k : } :
Polynomial.comp (p * Polynomial.X ^ k) r = * r ^ k
@[simp]
theorem Polynomial.C_mul_comp {R : Type u} {a : R} [] {p : } {r : } :
Polynomial.comp (Polynomial.C a * p) r = Polynomial.C a *
@[simp]
theorem Polynomial.nat_cast_mul_comp {R : Type u} [] {p : } {r : } {n : } :
Polynomial.comp (n * p) r = n *
theorem Polynomial.mul_X_add_nat_cast_comp {R : Type u} [] {p : } {q : } {n : } :
Polynomial.comp (p * (Polynomial.X + n)) q = * (q + n)
@[simp]
theorem Polynomial.mul_comp {R : Type u_1} [] (p : ) (q : ) (r : ) :
Polynomial.comp (p * q) r = *
@[simp]
theorem Polynomial.pow_comp {R : Type u_1} [] (p : ) (q : ) (n : ) :
Polynomial.comp (p ^ n) q = ^ n
@[simp]
theorem Polynomial.bit0_comp {R : Type u} [] {p : } {q : } :
@[simp]
theorem Polynomial.bit1_comp {R : Type u} [] {p : } {q : } :
@[simp]
theorem Polynomial.smul_comp {R : Type u} {S : Type v} [] [] [] [] (s : S) (p : ) (q : ) :
theorem Polynomial.comp_assoc {R : Type u_1} [] (φ : ) (ψ : ) (χ : ) :
=
theorem Polynomial.coeff_comp_degree_mul_degree {R : Type u} [] {p : } {q : } (hqd0 : ) :
@[simp]
theorem Polynomial.sum_comp {R : Type u} {ι : Type y} [] (s : ) (p : ι) (q : ) :
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} [] [] (f : R →+* S) :

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

Equations
Instances For
@[simp]
theorem Polynomial.map_C {R : Type u} {S : Type v} {a : R} [] [] (f : R →+* S) :
Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
@[simp]
theorem Polynomial.map_X {R : Type u} {S : Type v} [] [] (f : R →+* S) :
Polynomial.map f Polynomial.X = Polynomial.X
@[simp]
theorem Polynomial.map_monomial {R : Type u} {S : Type v} [] [] (f : R →+* S) {n : } {a : R} :
Polynomial.map f ( a) = (f a)
@[simp]
theorem Polynomial.map_zero {R : Type u} {S : Type v} [] [] (f : R →+* S) :
= 0
@[simp]
theorem Polynomial.map_add {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) :
Polynomial.map f (p + q) = +
@[simp]
theorem Polynomial.map_one {R : Type u} {S : Type v} [] [] (f : R →+* S) :
= 1
@[simp]
theorem Polynomial.map_mul {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) :
Polynomial.map f (p * q) = *
@[simp]
theorem Polynomial.map_smul {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (r : R) :
Polynomial.map f (r p) = f r
def Polynomial.mapRingHom {R : Type u} {S : Type v} [] [] (f : R →+* S) :

Polynomial.map as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Polynomial.coe_mapRingHom {R : Type u} {S : Type v} [] [] (f : R →+* S) :
@[simp]
theorem Polynomial.map_nat_cast {R : Type u} {S : Type v} [] [] (f : R →+* S) (n : ) :
= n
@[simp]
theorem Polynomial.map_ofNat {R : Type u} {S : Type v} [] [] (f : R →+* S) (n : ) [] :
@[simp]
theorem Polynomial.map_bit0 {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) :
@[simp]
theorem Polynomial.map_bit1 {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) :
theorem Polynomial.map_dvd {R : Type u} {S : Type v} [] [] (f : R →+* S) {x : } {y : } :
x y
@[simp]
theorem Polynomial.coeff_map {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (n : ) :
= f ()
@[simp]
theorem Polynomial.mapEquiv_symm_apply {R : Type u} {S : Type v} [] [] (e : R ≃+* S) (a : ) :
= Polynomial.map (()) a
@[simp]
theorem Polynomial.mapEquiv_apply {R : Type u} {S : Type v} [] [] (e : R ≃+* S) (a : ) :
a = Polynomial.map (e) a
def Polynomial.mapEquiv {R : Type u} {S : Type v} [] [] (e : R ≃+* S) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Polynomial.map_map {R : Type u} {S : Type v} {T : Type w} [] [] (f : R →+* S) [] (g : S →+* T) (p : ) :
@[simp]
theorem Polynomial.map_id {R : Type u} [] {p : } :
= p
theorem Polynomial.eval₂_eq_eval_map {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) {x : S} :
=
theorem Polynomial.map_injective {R : Type u} {S : Type v} [] [] (f : R →+* S) (hf : ) :
theorem Polynomial.map_surjective {R : Type u} {S : Type v} [] [] (f : R →+* S) (hf : ) :
theorem Polynomial.degree_map_le {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) :
theorem Polynomial.natDegree_map_le {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) :
theorem Polynomial.map_eq_zero_iff {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} (hf : ) :
= 0 p = 0
theorem Polynomial.map_ne_zero_iff {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} (hf : ) :
0 p 0
theorem Polynomial.map_monic_eq_zero_iff {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} (hp : ) :
= 0 ∀ (x : R), f x = 0
theorem Polynomial.map_monic_ne_zero {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} (hp : ) [] :
0
theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (hf : 0) :
theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (hf : 0) :
theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (hf : 0) :
@[simp]
theorem Polynomial.mapRingHom_id {R : Type u} [] :
@[simp]
theorem Polynomial.mapRingHom_comp {R : Type u} {S : Type v} {T : Type w} [] [] [] (f : S →+* T) (g : R →+* S) :
theorem Polynomial.map_list_prod {R : Type u} {S : Type v} [] [] (f : R →+* S) (L : List ()) :
@[simp]
theorem Polynomial.map_pow {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (n : ) :
Polynomial.map f (p ^ n) = ^ n
theorem Polynomial.mem_map_rangeS {R : Type u} {S : Type v} [] [] (f : R →+* S) {p : } :
∀ (n : ),
theorem Polynomial.mem_map_range {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {p : } :
∀ (n : ),
theorem Polynomial.eval₂_map {R : Type u} {S : Type v} {T : Type w} [] {p : } [] (f : R →+* S) [] (g : S →+* T) (x : T) :
theorem Polynomial.eval_map {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : S) :
=
theorem Polynomial.map_sum {R : Type u} {S : Type v} [] [] (f : R →+* S) {ι : Type u_1} (g : ι) (s : ) :
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} [] [] (f : R →+* S) (p : ) (q : ) :
@[simp]
theorem Polynomial.eval_zero_map {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) :
= f ()
@[simp]
theorem Polynomial.eval_one_map {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) :
= f ()
@[simp]
theorem Polynomial.eval_nat_cast_map {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) (n : ) :
Polynomial.eval (n) () = 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 : ) (i : ) :
Polynomial.eval (i) () = 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} [] (p : ) [] [] (f : R →+* S) (g : S →+* T) (x : S) :
g () = Polynomial.eval₂ () (g x) p
theorem Polynomial.eval₂_hom {R : Type u} {S : Type v} [] {p : } [] (f : R →+* S) (x : R) :
Polynomial.eval₂ f (f x) p = f ()
theorem Polynomial.eval₂_comp {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) {x : S} :
@[simp]
theorem Polynomial.iterate_comp_eval₂ {R : Type u} {S : Type v} [] {p : } {q : } [] (f : R →+* S) (k : ) (t : S) :
) = )^[k] ()
@[simp]
theorem Polynomial.eval₂_mul' {R : Type u} {S : Type v} [] [] [Algebra R S] (x : S) (p : ) (q : ) :
@[simp]
theorem Polynomial.eval₂_pow' {R : Type u} {S : Type v} [] [] [Algebra R S] (x : S) (p : ) (n : ) :
@[simp]
theorem Polynomial.eval₂_comp' {R : Type u} {S : Type v} [] [] [Algebra R S] (x : S) (p : ) (q : ) :
@[simp]
theorem Polynomial.eval_mul {R : Type u} [] {p : } {q : } {x : R} :
Polynomial.eval x (p * q) = *
def Polynomial.evalRingHom {R : Type u} [] :
R

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

Equations
• Polynomial.evalRingHom =
Instances For
@[simp]
theorem Polynomial.coe_evalRingHom {R : Type u} [] (r : R) :
theorem Polynomial.evalRingHom_zero :
= Polynomial.constantCoeff
@[simp]
theorem Polynomial.eval_pow {R : Type u} [] {p : } {x : R} (n : ) :
Polynomial.eval x (p ^ n) = ^ n
@[simp]
theorem Polynomial.eval_comp {R : Type u} [] {p : } {q : } {x : R} :
=
@[simp]
theorem Polynomial.iterate_comp_eval {R : Type u} [] {p : } {q : } (k : ) (t : R) :
) = )^[k] ()
theorem Polynomial.isRoot_comp {R : Type u_1} [] {p : } {q : } {r : R} :
def Polynomial.compRingHom {R : Type u} [] :

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

Equations
Instances For
@[simp]
theorem Polynomial.coe_compRingHom {R : Type u} [] (q : ) :
= fun (p : ) =>
theorem Polynomial.coe_compRingHom_apply {R : Type u} [] (p : ) (q : ) :
=
theorem Polynomial.root_mul_left_of_isRoot {R : Type u} {a : R} [] (p : ) {q : } :
Polynomial.IsRoot (p * q) a
theorem Polynomial.root_mul_right_of_isRoot {R : Type u} {a : R} [] {p : } (q : ) :
Polynomial.IsRoot (p * q) a
theorem Polynomial.eval₂_multiset_prod {R : Type u} {S : Type v} [] [] (f : R →+* S) (s : ) (x : S) :
theorem Polynomial.eval₂_finset_prod {R : Type u} {S : Type v} {ι : Type y} [] [] (f : R →+* S) (s : ) (g : ι) (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} [] (l : List ()) (x : R) :

Polynomial evaluation commutes with List.prod

theorem Polynomial.eval_multiset_prod {R : Type u} [] (s : ) (x : R) :

Polynomial evaluation commutes with Multiset.prod

theorem Polynomial.eval_prod {R : Type u} [] {ι : Type u_1} (s : ) (p : ι) (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} [] (l : List ()) (q : ) :
= List.prod (List.map (fun (p : ) => ) l)
theorem Polynomial.multiset_prod_comp {R : Type u} [] (s : ) (q : ) :
= Multiset.prod (Multiset.map (fun (p : ) => ) s)
theorem Polynomial.prod_comp {R : Type u} [] {ι : Type u_1} (s : ) (p : ι) (q : ) :
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} [] [] {ι : Type u_1} (s : ) (p : ι) (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} [] {p : } {q : } {x : R} :
p q
theorem Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero {R : Type u} [] {p : } {q : } {x : R} :
p q = 0 = 0
@[simp]
theorem Polynomial.eval_geom_sum {R : Type u_1} [] {n : } {x : R} :
Polynomial.eval x (Finset.sum () fun (i : ) => Polynomial.X ^ i) = Finset.sum () fun (i : ) => x ^ i
theorem Polynomial.support_map_subset {R : Type u} {S : Type v} [] [] (f : R →+* S) (p : ) :
theorem Polynomial.support_map_of_injective {R : Type u} {S : Type v} [] [] (p : ) {f : R →+* S} (hf : ) :
theorem Polynomial.map_multiset_prod {R : Type u} {S : Type v} [] [] (f : R →+* S) (m : ) :
=
theorem Polynomial.map_prod {R : Type u} {S : Type v} [] [] (f : R →+* S) {ι : Type u_1} (g : ι) (s : ) :
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} [] [] {f : R →+* S} {x : R} {p : } (h : ) :
theorem Polynomial.IsRoot.of_map {S : Type v} [] {R : Type u_1} [] {f : R →+* S} {x : R} {p : } (h : Polynomial.IsRoot () (f x)) (hf : ) :
theorem Polynomial.isRoot_map_iff {S : Type v} [] {R : Type u_1} [] {f : R →+* S} {x : R} {p : } (hf : ) :
@[simp]
theorem Polynomial.map_sub {R : Type u} [Ring R] {p : } {q : } {S : Type u_1} [Ring S] (f : R →+* S) :
Polynomial.map f (p - q) = -
@[simp]
theorem Polynomial.map_neg {R : Type u} [Ring R] {p : } {S : Type u_1} [Ring S] (f : R →+* S) :
@[simp]
theorem Polynomial.map_int_cast {R : Type u} [Ring R] {S : Type u_1} [Ring S] (f : R →+* S) (n : ) :
= n
@[simp]
theorem Polynomial.eval_int_cast {R : Type u} [Ring R] {n : } {x : R} :
= n
@[simp]
theorem Polynomial.eval₂_neg {R : Type u} [Ring R] {p : } {S : Type u_1} [Ring S] (f : R →+* S) {x : S} :
@[simp]
theorem Polynomial.eval₂_sub {R : Type u} [Ring R] {p : } {q : } {S : Type u_1} [Ring S] (f : R →+* S) {x : S} :
Polynomial.eval₂ f x (p - q) = -
@[simp]
theorem Polynomial.eval_neg {R : Type u} [Ring R] (p : ) (x : R) :
@[simp]
theorem Polynomial.eval_sub {R : Type u} [Ring R] (p : ) (q : ) (x : R) :
Polynomial.eval x (p - 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 : } {q : } :
@[simp]
theorem Polynomial.sub_comp {R : Type u} [Ring R] {p : } {q : } {r : } :
Polynomial.comp (p - q) r = -
@[simp]
theorem Polynomial.cast_int_comp {R : Type u} [Ring R] {p : } (i : ) :
Polynomial.comp (i) p = i
@[simp]
theorem Polynomial.eval₂_at_int_cast {R : Type u} [Ring R] {p : } {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 : } {q : } {n : } :
Polynomial.comp (p * (Polynomial.X - n)) q = * (q - n)