Documentation

Mathlib.Algebra.Polynomial.Eval.Coeff

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_of_coeff_zero_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.coeff 0 = 0) :
p.IsRoot 0
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
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_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_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
    @[deprecated Polynomial.eval_natCast_map (since := "2024-04-17")]
    theorem Polynomial.eval_nat_cast_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)

    Alias of Polynomial.eval_natCast_map.

    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
    @[deprecated Polynomial.eval_intCast_map (since := "2024-04-17")]
    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 : ℤ) :
    eval (↑i) (map f p) = f (eval (↑i) p)

    Alias of Polynomial.eval_intCast_map.

    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} [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
    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