Evaluation of polynomials

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

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem Polynomial.map_id {R : Type u} [Semiring R] {p : Polynomial R} : 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.map_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (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 (map f)

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

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

@[simp]

theorem Polynomial.mapRingHom_id {R : Type u} [Semiring R] : 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) : (mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g)

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

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

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

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

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

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

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)

theorem Polynomial.evalRingHom_zero : evalRingHom 0 = constantCoeff

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

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

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

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

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