mathlib3 documentation

data.polynomial.eval

Theory of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The main defs here are eval₂, eval, and map. We give several lemmas about their interaction with each other and with module operations.

source
@[irreducible]
def polynomial.eval₂ {R : Type u} {S : Type v} [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
source
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 (λ (e : ℕ) (a : R), ⇑f a * x ^ e)
source
theorem polynomial.eval₂_congr {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {f g : R →+* S} {s t : S} {φ ψ : polynomial R} :
f = g → s = t → φ = ψ → polynomial.eval₂ f s φ = polynomial.eval₂ g t ψ
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem polynomial.eval₂_add {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) (x : S) :
polynomial.eval₂ f x (p + q) = polynomial.eval₂ f x p + polynomial.eval₂ f x q
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[simp]
theorem polynomial.eval₂_C_X {R : Type u} [semiring R] {p : polynomial R} :
polynomial.eval₂ polynomial.C polynomial.X p = p
source
def polynomial.eval₂_add_monoid_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) :
polynomial R →+ S

eval₂_add_monoid_hom (f : R →+* S) (x : S) is the add_monoid_hom from R[X] to S obtained by evaluating the pushforward of p along f at x.

Equations
source
@[simp]
theorem polynomial.eval₂_add_monoid_hom_apply {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (x : S) (p : polynomial R) :
⇑(polynomial.eval₂_add_monoid_hom f x) p = polynomial.eval₂ f x p
source
@[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
source
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 (λ (n : ℕ) (a : T), polynomial.eval₂ f x (g n a))
source
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
source
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
source
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 (s.sum (λ (i : ι), g i)) = s.sum (λ (i : ι), polynomial.eval₂ f x (g i))
source
theorem polynomial.eval₂_of_finsupp {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} {x : S} {p : add_monoid_algebra R ℕ} :
polynomial.eval₂ f x {to_finsupp := p} = ⇑(add_monoid_algebra.lift_nc ↑f ⇑(⇑(powers_hom S) x)) p
source
theorem polynomial.eval₂_mul_noncomm {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) (x : S) (hf : ∀ (k : ℕ), commute (⇑f (q.coeff k)) x) :
polynomial.eval₂ f x (p * q) = polynomial.eval₂ f x p * polynomial.eval₂ f x q
source
@[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
source
@[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
source
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
source
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 : polynomial R), p ∈ ps → ∀ (k : ℕ), commute (⇑f (p.coeff k)) x) :
polynomial.eval₂ f x ps.prod = (list.map (polynomial.eval₂ f x) ps).prod
source
def polynomial.eval₂_ring_hom' {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 ring_hom for noncommutative rings

Equations

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

source
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.range (p.nat_degree + 1)).sum (λ (i : ℕ), ⇑f (p.coeff i) * x ^ i)
source
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.nat_degree < n) (x : S) :
polynomial.eval₂ f x p = (finset.range n).sum (λ (i : ℕ), ⇑f (p.coeff i) * x ^ i)
source
@[simp]
theorem polynomial.eval₂_mul {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) :
polynomial.eval₂ f x (p * q) = polynomial.eval₂ f x p * polynomial.eval₂ f x q
source
theorem polynomial.eval₂_mul_eq_zero_of_left {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) (q : polynomial R) (hp : polynomial.eval₂ f x p = 0) :
polynomial.eval₂ f x (p * q) = 0
source
theorem polynomial.eval₂_mul_eq_zero_of_right {R : Type u} {S : Type v} [semiring R] {q : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) (p : polynomial R) (hq : polynomial.eval₂ f x q = 0) :
polynomial.eval₂ f x (p * q) = 0
source
noncomputable def polynomial.eval₂_ring_hom {R : Type u} {S : Type v} [semiring R] [comm_semiring S] (f : R →+* S) (x : S) :
polynomial R →+* S

eval₂ as a ring_hom

Equations
source
@[simp]
theorem polynomial.coe_eval₂_ring_hom {R : Type u} {S : Type v} [semiring R] [comm_semiring S] (f : R →+* S) (x : S) :
⇑(polynomial.eval₂_ring_hom f x) = polynomial.eval₂ f x
source
theorem polynomial.eval₂_pow {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) (n : ℕ) :
polynomial.eval₂ f x (p ^ n) = polynomial.eval₂ f x p ^ n
source
theorem polynomial.eval₂_dvd {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) :
p ∣ q → polynomial.eval₂ f x p ∣ polynomial.eval₂ f x q
source
theorem polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [comm_semiring S] (f : R →+* S) (x : S) (h : p ∣ q) (h0 : polynomial.eval₂ f x p = 0) :
polynomial.eval₂ f x q = 0
source
theorem polynomial.eval₂_list_prod {R : Type u} {S : Type v} [semiring R] [comm_semiring S] (f : R →+* S) (l : list (polynomial R)) (x : S) :
polynomial.eval₂ f x l.prod = (list.map (polynomial.eval₂ f x) l).prod
source
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
source
theorem polynomial.eval_eq_sum {R : Type u} [semiring R] {p : polynomial R} {x : R} :
polynomial.eval x p = p.sum (λ (e : ℕ) (a : R), a * x ^ e)
source
theorem polynomial.eval_eq_sum_range {R : Type u} [semiring R] {p : polynomial R} (x : R) :
polynomial.eval x p = (finset.range (p.nat_degree + 1)).sum (λ (i : ℕ), p.coeff i * x ^ i)
source
theorem polynomial.eval_eq_sum_range' {R : Type u} [semiring R] {p : polynomial R} {n : ℕ} (hn : p.nat_degree < n) (x : R) :
polynomial.eval x p = (finset.range n).sum (λ (i : ℕ), p.coeff i * x ^ i)
source
@[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)
source
@[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)
source
@[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)
source
@[simp]
theorem polynomial.eval_C {R : Type u} {a : R} [semiring R] {x : R} :
polynomial.eval x (⇑polynomial.C a) = a
source
@[simp]
theorem polynomial.eval_nat_cast {R : Type u} [semiring R] {x : R} {n : ℕ} :
polynomial.eval x ↑n = ↑n
source
@[simp]
theorem polynomial.eval_X {R : Type u} [semiring R] {x : R} :
polynomial.eval x polynomial.X = x
source
@[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
source
@[simp]
theorem polynomial.eval_zero {R : Type u} [semiring R] {x : R} :
polynomial.eval x 0 = 0
source
@[simp]
theorem polynomial.eval_add {R : Type u} [semiring R] {p q : polynomial R} {x : R} :
polynomial.eval x (p + q) = polynomial.eval x p + polynomial.eval x q
source
@[simp]
theorem polynomial.eval_one {R : Type u} [semiring R] {x : R} :
polynomial.eval x 1 = 1
source
@[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)
source
@[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)
source
@[simp]
theorem polynomial.eval_smul {R : Type u} {S : Type v} [semiring R] [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) (p : polynomial R) (x : R) :
polynomial.eval x (s • p) = s • polynomial.eval x p
source
@[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
source
theorem polynomial.eval_monomial_one_add_sub {S : Type v} [comm_ring S] (d : ℕ) (y : S) :
polynomial.eval (1 + y) (⇑(polynomial.monomial d) (↑d + 1)) - polynomial.eval y (⇑(polynomial.monomial d) (↑d + 1)) = (finset.range (d + 1)).sum (λ (x_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 {d + 1 \choose i} \cdot i \cdot y^{i - 1}.$$

source
@[simp]
theorem polynomial.leval_apply {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
⇑(polynomial.leval r) f = polynomial.eval r f
source
def polynomial.leval {R : Type u_1} [semiring R] (r : R) :
polynomial R →ₗ[R] R

polynomial.eval as linear map

Equations
source
@[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
source
@[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
source
@[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
source
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 (λ (n : ℕ) (a : R), polynomial.eval x (f n a))
source
theorem polynomial.eval_finset_sum {R : Type u} {ι : Type y} [semiring R] (s : finset ι) (g : ι → polynomial R) (x : R) :
polynomial.eval x (s.sum (λ (i : ι), g i)) = s.sum (λ (i : ι), polynomial.eval x (g i))
source
def polynomial.is_root {R : Type u} [semiring R] (p : polynomial R) (a : R) :
Prop

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

Equations
Instances for polynomial.is_root
source
@[protected, instance]
def polynomial.is_root.decidable {R : Type u} {a : R} [semiring R] {p : polynomial R} [decidable_eq R] :
decidable (p.is_root a)
Equations
source
@[simp]
theorem polynomial.is_root.def {R : Type u} {a : R} [semiring R] {p : polynomial R} :
p.is_root a ↔ polynomial.eval a p = 0
source
theorem polynomial.is_root.eq_zero {R : Type u} [semiring R] {p : polynomial R} {x : R} (h : p.is_root x) :
polynomial.eval x p = 0
source
theorem polynomial.coeff_zero_eq_eval_zero {R : Type u} [semiring R] (p : polynomial R) :
p.coeff 0 = polynomial.eval 0 p
source
theorem polynomial.zero_is_root_of_coeff_zero_eq_zero {R : Type u} [semiring R] {p : polynomial R} (hp : p.coeff 0 = 0) :
p.is_root 0
source
theorem polynomial.is_root.dvd {R : Type u_1} [comm_semiring R] {p q : polynomial R} {x : R} (h : p.is_root x) (hpq : p ∣ q) :
q.is_root x
source
theorem polynomial.not_is_root_C {R : Type u} [semiring R] (r a : R) (hr : r ≠ 0) :
¬(⇑polynomial.C r).is_root a
source
theorem polynomial.eval_surjective {R : Type u} [semiring R] (x : R) :
function.surjective (polynomial.eval x)
source
noncomputable def polynomial.comp {R : Type u} [semiring R] (p q : polynomial R) :
polynomial R

The composition of polynomials as a polynomial.

Equations
source
theorem polynomial.comp_eq_sum_left {R : Type u} [semiring R] {p q : polynomial R} :
p.comp q = p.sum (λ (e : ℕ) (a : R), ⇑polynomial.C a * q ^ e)
source
@[simp]
theorem polynomial.comp_X {R : Type u} [semiring R] {p : polynomial R} :
p.comp polynomial.X = p
source
@[simp]
theorem polynomial.X_comp {R : Type u} [semiring R] {p : polynomial R} :
polynomial.X.comp p = p
source
@[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)
source
@[simp]
theorem polynomial.C_comp {R : Type u} {a : R} [semiring R] {p : polynomial R} :
(⇑polynomial.C a).comp p = ⇑polynomial.C a
source
@[simp]
theorem polynomial.nat_cast_comp {R : Type u} [semiring R] {p : polynomial R} {n : ℕ} :
↑n.comp p = ↑n
source
@[simp]
theorem polynomial.comp_zero {R : Type u} [semiring R] {p : polynomial R} :
p.comp 0 = ⇑polynomial.C (polynomial.eval 0 p)
source
@[simp]
theorem polynomial.zero_comp {R : Type u} [semiring R] {p : polynomial R} :
0.comp p = 0
source
@[simp]
theorem polynomial.comp_one {R : Type u} [semiring R] {p : polynomial R} :
p.comp 1 = ⇑polynomial.C (polynomial.eval 1 p)
source
@[simp]
theorem polynomial.one_comp {R : Type u} [semiring R] {p : polynomial R} :
1.comp p = 1
source
@[simp]
theorem polynomial.add_comp {R : Type u} [semiring R] {p q r : polynomial R} :
(p + q).comp r = p.comp r + q.comp r
source
@[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
source
@[simp]
theorem polynomial.mul_X_comp {R : Type u} [semiring R] {p r : polynomial R} :
(p * polynomial.X).comp r = p.comp r * r
source
@[simp]
theorem polynomial.X_pow_comp {R : Type u} [semiring R] {p : polynomial R} {k : ℕ} :
(polynomial.X ^ k).comp p = p ^ k
source
@[simp]
theorem polynomial.mul_X_pow_comp {R : Type u} [semiring R] {p r : polynomial R} {k : ℕ} :
(p * polynomial.X ^ k).comp r = p.comp r * r ^ k
source
@[simp]
theorem polynomial.C_mul_comp {R : Type u} {a : R} [semiring R] {p r : polynomial R} :
(⇑polynomial.C a * p).comp r = ⇑polynomial.C a * p.comp r
source
@[simp]
theorem polynomial.nat_cast_mul_comp {R : Type u} [semiring R] {p r : polynomial R} {n : ℕ} :
(↑n * p).comp r = ↑n * p.comp r
source
@[simp]
theorem polynomial.mul_comp {R : Type u_1} [comm_semiring R] (p q r : polynomial R) :
(p * q).comp r = p.comp r * q.comp r
source
@[simp]
theorem polynomial.pow_comp {R : Type u_1} [comm_semiring R] (p q : polynomial R) (n : ℕ) :
(p ^ n).comp q = p.comp q ^ n
source
@[simp]
theorem polynomial.bit0_comp {R : Type u} [semiring R] {p q : polynomial R} :
(bit0 p).comp q = bit0 (p.comp q)
source
@[simp]
theorem polynomial.bit1_comp {R : Type u} [semiring R] {p q : polynomial R} :
(bit1 p).comp q = bit1 (p.comp q)
source
@[simp]
theorem polynomial.smul_comp {R : Type u} {S : Type v} [semiring R] [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) (p q : polynomial R) :
(s • p).comp q = s • p.comp q
source
theorem polynomial.comp_assoc {R : Type u_1} [comm_semiring R] (φ ψ χ : polynomial R) :
(φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
source
theorem polynomial.coeff_comp_degree_mul_degree {R : Type u} [semiring R] {p q : polynomial R} (hqd0 : q.nat_degree ≠ 0) :
(p.comp q).coeff (p.nat_degree * q.nat_degree) = p.leading_coeff * q.leading_coeff ^ p.nat_degree
source
noncomputable 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
source
@[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)
source
@[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
source
@[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)
source
@[protected, simp]
theorem polynomial.map_zero {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
polynomial.map f 0 = 0
source
@[protected, simp]
theorem polynomial.map_add {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) :
polynomial.map f (p + q) = polynomial.map f p + polynomial.map f q
source
@[protected, simp]
theorem polynomial.map_one {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
polynomial.map f 1 = 1
source
@[protected, simp]
theorem polynomial.map_mul {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [semiring S] (f : R →+* S) :
polynomial.map f (p * q) = polynomial.map f p * polynomial.map f q
source
@[protected, 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
source
noncomputable def polynomial.map_ring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
polynomial R →+* polynomial S

polynomial.map as a ring_hom.

Equations
source
@[simp]
theorem polynomial.coe_map_ring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
⇑(polynomial.map_ring_hom f) = polynomial.map f
source
@[protected, 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
source
@[protected, 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)
source
@[protected, 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)
source
theorem polynomial.map_dvd {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) {x y : polynomial R} :
x ∣ y → polynomial.map f x ∣ polynomial.map f y
source
@[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)
source
noncomputable def polynomial.map_equiv {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
source
@[simp]
theorem polynomial.map_equiv_apply {R : Type u} {S : Type v} [semiring R] [semiring S] (e : R ≃+* S) (a : polynomial R) :
⇑(polynomial.map_equiv e) a = polynomial.map ↑e a
source
@[simp]
theorem polynomial.map_equiv_symm_apply {R : Type u} {S : Type v} [semiring R] [semiring S] (e : R ≃+* S) (a : polynomial S) :
⇑((polynomial.map_equiv e).symm) a = polynomial.map ↑(e.symm) a
source
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
source
@[simp]
theorem polynomial.map_id {R : Type u} [semiring R] {p : polynomial R} :
polynomial.map (ring_hom.id R) p = p
source
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)
source
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)
source
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)
source
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
source
theorem polynomial.nat_degree_map_le {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (p : polynomial R) :
(polynomial.map f p).nat_degree ≤ p.nat_degree
source
@[protected]
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
source
@[protected]
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
source
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
source
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
source
theorem polynomial.degree_map_eq_of_leading_coeff_ne_zero {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hf : ⇑f p.leading_coeff ≠ 0) :
(polynomial.map f p).degree = p.degree
source
theorem polynomial.nat_degree_map_of_leading_coeff_ne_zero {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hf : ⇑f p.leading_coeff ≠ 0) :
(polynomial.map f p).nat_degree = p.nat_degree
source
theorem polynomial.leading_coeff_map_of_leading_coeff_ne_zero {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hf : ⇑f p.leading_coeff ≠ 0) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
source
@[simp]
theorem polynomial.map_ring_hom_id {R : Type u} [semiring R] :
polynomial.map_ring_hom (ring_hom.id R) = ring_hom.id (polynomial R)
source
@[simp]
theorem polynomial.map_ring_hom_comp {R : Type u} {S : Type v} {T : Type w} [semiring R] [semiring S] [semiring T] (f : S →+* T) (g : R →+* S) :
(polynomial.map_ring_hom f).comp (polynomial.map_ring_hom g) = polynomial.map_ring_hom (f.comp g)
source
@[protected]
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
source
@[protected, 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
source
theorem polynomial.mem_map_srange {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) {p : polynomial S} :
p ∈ (polynomial.map_ring_hom f).srange ↔ ∀ (n : ℕ), p.coeff n ∈ f.srange
source
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.map_ring_hom f).range ↔ ∀ (n : ℕ), p.coeff n ∈ f.range
source
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
source
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
source
@[protected]
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 (s.sum (λ (i : ι), g i)) = s.sum (λ (i : ι), polynomial.map f (g i))
source
theorem polynomial.map_comp {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (p q : polynomial R) :
polynomial.map f (p.comp q) = (polynomial.map f p).comp (polynomial.map f q)
source
@[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)
source
@[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)
source
@[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)
source
@[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?

source
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
source
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)
source
theorem polynomial.eval₂_comp {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [comm_semiring S] (f : R →+* S) {x : S} :
polynomial.eval₂ f x (p.comp q) = polynomial.eval₂ f (polynomial.eval₂ f x q) p
source
@[simp]
theorem polynomial.iterate_comp_eval₂ {R : Type u} {S : Type v} [semiring R] {p q : polynomial R} [comm_semiring S] (f : R →+* S) (k : ℕ) (t : S) :
polynomial.eval₂ f t (p.comp^[k] q) = (λ (x : S), polynomial.eval₂ f x p)^[k] (polynomial.eval₂ f t q)
source
@[simp]
theorem polynomial.eval_mul {R : Type u} [comm_semiring R] {p q : polynomial R} {x : R} :
polynomial.eval x (p * q) = polynomial.eval x p * polynomial.eval x q
source
noncomputable def polynomial.eval_ring_hom {R : Type u} [comm_semiring R] :
R → polynomial R →+* R

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

Equations
source
@[simp]
theorem polynomial.coe_eval_ring_hom {R : Type u} [comm_semiring R] (r : R) :
⇑(polynomial.eval_ring_hom r) = polynomial.eval r
source
theorem polynomial.eval_ring_hom_zero  :
polynomial.eval_ring_hom 0 = polynomial.constant_coeff
source
@[simp]
theorem polynomial.eval_pow {R : Type u} [comm_semiring R] {p : polynomial R} {x : R} (n : ℕ) :
polynomial.eval x (p ^ n) = polynomial.eval x p ^ n
source
@[simp]
theorem polynomial.eval_comp {R : Type u} [comm_semiring R] {p q : polynomial R} {x : R} :
polynomial.eval x (p.comp q) = polynomial.eval (polynomial.eval x q) p
source
@[simp]
theorem polynomial.iterate_comp_eval {R : Type u} [comm_semiring R] {p q : polynomial R} (k : ℕ) (t : R) :
polynomial.eval t (p.comp^[k] q) = (λ (x : R), polynomial.eval x p)^[k] (polynomial.eval t q)
source
noncomputable def polynomial.comp_ring_hom {R : Type u} [comm_semiring R] :
polynomial R → polynomial R →+* polynomial R

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

Equations
source
@[simp]
theorem polynomial.coe_comp_ring_hom {R : Type u} [comm_semiring R] (q : polynomial R) :
⇑(q.comp_ring_hom) = λ (p : polynomial R), p.comp q
source
theorem polynomial.coe_comp_ring_hom_apply {R : Type u} [comm_semiring R] (p q : polynomial R) :
⇑(q.comp_ring_hom) p = p.comp q
source
theorem polynomial.root_mul_left_of_is_root {R : Type u} {a : R} [comm_semiring R] (p : polynomial R) {q : polynomial R} :
q.is_root a → (p * q).is_root a
source
theorem polynomial.root_mul_right_of_is_root {R : Type u} {a : R} [comm_semiring R] {p : polynomial R} (q : polynomial R) :
p.is_root a → (p * q).is_root a
source
theorem polynomial.eval₂_multiset_prod {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (f : R →+* S) (s : multiset (polynomial R)) (x : S) :
polynomial.eval₂ f x s.prod = (multiset.map (polynomial.eval₂ f x) s).prod
source
theorem polynomial.eval₂_finset_prod {R : Type u} {S : Type v} {ι : Type y} [comm_semiring R] [comm_semiring S] (f : R →+* S) (s : finset ι) (g : ι → polynomial R) (x : S) :
polynomial.eval₂ f x (s.prod (λ (i : ι), g i)) = s.prod (λ (i : ι), polynomial.eval₂ f x (g i))
source
theorem polynomial.eval_list_prod {R : Type u} [comm_semiring 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

source
theorem polynomial.eval_multiset_prod {R : Type u} [comm_semiring 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

source
theorem polynomial.eval_prod {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (p : ι → polynomial R) (x : R) :
polynomial.eval x (s.prod (λ (j : ι), p j)) = s.prod (λ (j : ι), polynomial.eval x (p j))

Polynomial evaluation commutes with finset.prod

source
theorem polynomial.list_prod_comp {R : Type u} [comm_semiring R] (l : list (polynomial R)) (q : polynomial R) :
l.prod.comp q = (list.map (λ (p : polynomial R), p.comp q) l).prod
source
theorem polynomial.multiset_prod_comp {R : Type u} [comm_semiring R] (s : multiset (polynomial R)) (q : polynomial R) :
s.prod.comp q = (multiset.map (λ (p : polynomial R), p.comp q) s).prod
source
theorem polynomial.prod_comp {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (p : ι → polynomial R) (q : polynomial R) :
(s.prod (λ (j : ι), p j)).comp q = s.prod (λ (j : ι), (p j).comp q)
source
theorem polynomial.is_root_prod {R : Type u_1} [comm_ring R] [is_domain R] {ι : Type u_2} (s : finset ι) (p : ι → polynomial R) (x : R) :
(s.prod (λ (j : ι), p j)).is_root x ↔ ∃ (i : ι) (H : i ∈ s), (p i).is_root x
source
theorem polynomial.eval_dvd {R : Type u} [comm_semiring R] {p q : polynomial R} {x : R} :
p ∣ q → polynomial.eval x p ∣ polynomial.eval x q
source
theorem polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero {R : Type u} [comm_semiring R] {p q : polynomial R} {x : R} :
p ∣ q → polynomial.eval x p = 0 → polynomial.eval x q = 0
source
@[simp]
theorem polynomial.eval_geom_sum {R : Type u_1} [comm_semiring R] {n : ℕ} {x : R} :
polynomial.eval x ((finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)) = (finset.range n).sum (λ (i : ℕ), x ^ i)
source
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
source
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
source
@[protected]
theorem polynomial.map_multiset_prod {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (f : R →+* S) (m : multiset (polynomial R)) :
polynomial.map f m.prod = (multiset.map (polynomial.map f) m).prod
source
@[protected]
theorem polynomial.map_prod {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (f : R →+* S) {ι : Type u_1} (g : ι → polynomial R) (s : finset ι) :
polynomial.map f (s.prod (λ (i : ι), g i)) = s.prod (λ (i : ι), polynomial.map f (g i))
source
theorem polynomial.is_root.map {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] {f : R →+* S} {x : R} {p : polynomial R} (h : p.is_root x) :
(polynomial.map f p).is_root (⇑f x)
source
theorem polynomial.is_root.of_map {S : Type v} [comm_semiring S] {R : Type u_1} [comm_ring R] {f : R →+* S} {x : R} {p : polynomial R} (h : (polynomial.map f p).is_root (⇑f x)) (hf : function.injective ⇑f) :
p.is_root x
source
theorem polynomial.is_root_map_iff {S : Type v} [comm_semiring S] {R : Type u_1} [comm_ring R] {f : R →+* S} {x : R} {p : polynomial R} (hf : function.injective ⇑f) :
(polynomial.map f p).is_root (⇑f x) ↔ p.is_root x
source
theorem polynomial.C_neg {R : Type u} {a : R} [ring R] :
⇑polynomial.C (-a) = -⇑polynomial.C a
source
theorem polynomial.C_sub {R : Type u} {a b : R} [ring R] :
⇑polynomial.C (a - b) = ⇑polynomial.C a - ⇑polynomial.C b
source
@[protected, simp]
theorem polynomial.map_sub {R : Type u} [ring R] {p q : polynomial R} {S : Type u_1} [ring S] (f : R →+* S) :
polynomial.map f (p - q) = polynomial.map f p - polynomial.map f q
source
@[protected, 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
source
@[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
source
@[simp]
theorem polynomial.eval_int_cast {R : Type u} [ring R] {n : ℤ} {x : R} :
polynomial.eval x ↑n = ↑n
source
@[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
source
@[simp]
theorem polynomial.eval₂_sub {R : Type u} [ring R] {p q : polynomial R} {S : Type u_1} [ring S] (f : R →+* S) {x : S} :
polynomial.eval₂ f x (p - q) = polynomial.eval₂ f x p - polynomial.eval₂ f x q
source
@[simp]
theorem polynomial.eval_neg {R : Type u} [ring R] (p : polynomial R) (x : R) :
polynomial.eval x (-p) = -polynomial.eval x p
source
@[simp]
theorem polynomial.eval_sub {R : Type u} [ring R] (p q : polynomial R) (x : R) :
polynomial.eval x (p - q) = polynomial.eval x p - polynomial.eval x q
source
theorem polynomial.root_X_sub_C {R : Type u} {a b : R} [ring R] :
(polynomial.X - ⇑polynomial.C a).is_root b ↔ a = b
source
@[simp]
theorem polynomial.neg_comp {R : Type u} [ring R] {p q : polynomial R} :
(-p).comp q = -p.comp q
source
@[simp]
theorem polynomial.sub_comp {R : Type u} [ring R] {p q r : polynomial R} :
(p - q).comp r = p.comp r - q.comp r
source
@[simp]
theorem polynomial.cast_int_comp {R : Type u} [ring R] {p : polynomial R} (i : ℤ) :
↑i.comp p = ↑i