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) : Polynomial.eval₂ f 0 p = f (p.coeff 0)

@[simp]

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

theorem Polynomial.coeff_zero_eq_eval_zero {R : Type u} [Semiring R] (p : Polynomial R) : p.coeff 0 = Polynomial.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 : ℕ) : (Polynomial.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) : (Polynomial.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) : Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp 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.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.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

@[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) : (Polynomial.mapRingHom f).comp (Polynomial.mapRingHom g) = Polynomial.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) : Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.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) : 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_natCast_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)

@[deprecated Polynomial.eval_natCast_map]

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)

Alias of Polynomial.eval_natCast_map.

@[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 : ℤ) : Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)

@[deprecated Polynomial.eval_intCast_map]

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)

Alias of Polynomial.eval_intCast_map.

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

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.evalRingHom_zero : Polynomial.evalRingHom 0 = Polynomial.constantCoeff

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

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

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) : (Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x