# Evaluation of polynomials #

This file contains results on the interaction of `Polynomial.eval` and `Polynomial.coeff`

source
@[simp]
theorem Polynomial.eval₂_at_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) :
eval₂ f 0 p = f (p.coeff 0)
source
@[simp]
theorem Polynomial.eval₂_C_X {R : Type u} [Semiring R] {p : Polynomial R} :
eval₂ C X p = p
source
theorem Polynomial.coeff_zero_eq_eval_zero {R : Type u} [Semiring R] (p : Polynomial R) :
p.coeff 0 = eval 0 p
source
theorem Polynomial.zero_isRoot_iff_coeff_zero_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.IsRoot 0 ↔ p.coeff 0 = 0
source
theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.coeff 0 = 0 → p.IsRoot 0

Alias of the reverse direction of `Polynomial.zero_isRoot_iff_coeff_zero_eq_zero`.

source
theorem Polynomial.coeff_zero_eq_zero_of_zero_isRoot {R : Type u} [Semiring R] {p : Polynomial R} :
p.IsRoot 0 → p.coeff 0 = 0

Alias of the forward direction of `Polynomial.zero_isRoot_iff_coeff_zero_eq_zero`.

source
@[simp]
theorem Polynomial.coeff_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ℕ) :
(map f p).coeff n = f (p.coeff n)
source
theorem Polynomial.coeff_map_eq_comp {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) :
(map f p).coeff = ⇑f ∘ p.coeff
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) :
map g (map f p) = map (g.comp f) p
source
@[simp]
theorem Polynomial.map_id {R : Type u} [Semiring R] {p : Polynomial R} :
map (RingHom.id R) p = p
source
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)) ⋯

Instances For

source
theorem Polynomial.map_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Injective ⇑f) :
Function.Injective (map f)
source
theorem Polynomial.map_injective_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
Function.Injective (map f) ↔ Function.Injective ⇑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 (map f)
source
theorem Polynomial.map_surjective_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
Function.Surjective (map f) ↔ Function.Surjective ⇑f
source
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) :
map f p = 0 ↔ p = 0
source
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) :
map f p ≠ 0 ↔ p ≠ 0
source
@[simp]
theorem Polynomial.mapRingHom_id {R : Type u} [Semiring R] :
mapRingHom (RingHom.id R) = RingHom.id (Polynomial R)
source
@[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) :
(mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g)
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) :
eval₂ g x (map f p) = eval₂ (g.comp f) x p
source
@[simp]
theorem Polynomial.eval_zero_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) :
eval 0 (map f p) = f (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) :
eval 1 (map f p) = f (eval 1 p)
source
@[simp]
theorem Polynomial.eval_natCast_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ) :
eval (↑n) (map f p) = f (eval (↑n) p)
source
@[simp]
theorem Polynomial.eval_intCast_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (p : Polynomial R) (i : ℤ) :
eval (↑i) (map f p) = f (eval (↑i) p)
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 (eval₂ f x p) = 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) :
eval₂ f (f x) p = f (eval x p)
source
theorem Polynomial.evalRingHom_zero :
evalRingHom 0 = constantCoeff
source
theorem Polynomial.support_map_subset {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) :
(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) :
(map f p).support = p.support
source
theorem Polynomial.IsRoot.map {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R} (h : p.IsRoot x) :
(Polynomial.map f p).IsRoot (f x)
source
theorem Polynomial.IsRoot.of_map {S : Type v} [CommSemiring S] {R : Type u_1} [Ring R] {f : R →+* S} {x : R} {p : Polynomial R} (h : (Polynomial.map f p).IsRoot (f x)) (hf : Function.Injective ⇑f) :
p.IsRoot x
source
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) :
(map f p).IsRoot (f x) ↔ p.IsRoot x