Documentation

Mathlib.Data.Polynomial.Eval

Theory of univariate polynomials #

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

theorem Polynomial.eval₂_def {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) :
Polynomial.eval₂ f x p = Polynomial.sum p fun e a => f a * x ^ e
@[irreducible]
def Polynomial.eval₂ {R : Type u_1} {S : Type u_2} [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

Instances For
    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 = Polynomial.sum p fun e a => f a * x ^ e
    theorem Polynomial.eval₂_congr {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} {g : R →+* S} {s : S} {t : S} {φ : Polynomial R} {ψ : Polynomial R} :
    f = gs = tφ = ψPolynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ
    @[simp]
    theorem Polynomial.eval₂_at_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) :
    @[simp]
    theorem Polynomial.eval₂_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :
    @[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
    @[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
    @[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
    @[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
    @[simp]
    theorem Polynomial.eval₂_add {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
    @[simp]
    theorem Polynomial.eval₂_one {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :
    @[simp]
    theorem Polynomial.eval₂_bit0 {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
    @[simp]
    theorem Polynomial.eval₂_bit1 {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
    @[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} :
    @[simp]
    theorem Polynomial.eval₂_C_X {R : Type u} [Semiring R] {p : Polynomial R} :
    Polynomial.eval₂ Polynomial.C Polynomial.X p = p
    @[simp]
    theorem Polynomial.eval₂AddMonoidHom_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) :
    def Polynomial.eval₂AddMonoidHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) :

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

    Instances For
      @[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
      @[simp]
      theorem Polynomial.eval₂_ofNat {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] (n : ) [Nat.AtLeastTwo n] (f : R →+* S) (a : S) :
      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 : TPolynomial R) (x : S) :
      theorem Polynomial.eval₂_list_sum {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S) :
      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 (Finset.sum s fun i => g i) = Finset.sum s fun i => Polynomial.eval₂ f x (g i)
      theorem Polynomial.eval₂_ofFinsupp {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {x : S} {p : AddMonoidAlgebra R } :
      Polynomial.eval₂ f x { toFinsupp := p } = ↑(AddMonoidAlgebra.liftNC f ↑(↑(powersHom S) x)) p
      theorem Polynomial.eval₂_mul_noncomm {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (k : ), Commute (f (Polynomial.coeff q k)) x) :
      @[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
      @[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
      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
      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 (Polynomial.coeff p k)) x) :
      def Polynomial.eval₂RingHom' {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) :

      eval₂ as a RingHom for noncommutative rings

      Instances For

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

        theorem Polynomial.eval₂_eq_sum_range {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
        theorem Polynomial.eval₂_eq_sum_range' {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : } (hn : Polynomial.natDegree p < n) (x : S) :
        Polynomial.eval₂ f x p = Finset.sum (Finset.range n) fun i => f (Polynomial.coeff p i) * x ^ i
        @[simp]
        theorem Polynomial.eval₂_mul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) :
        theorem Polynomial.eval₂_mul_eq_zero_of_left {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (q : Polynomial R) (hp : Polynomial.eval₂ f x p = 0) :
        Polynomial.eval₂ f x (p * q) = 0
        theorem Polynomial.eval₂_mul_eq_zero_of_right {R : Type u} {S : Type v} [Semiring R] {q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hq : Polynomial.eval₂ f x q = 0) :
        Polynomial.eval₂ f x (p * q) = 0
        def Polynomial.eval₂RingHom {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) :

        eval₂ as a RingHom

        Instances For
          @[simp]
          theorem Polynomial.coe_eval₂RingHom {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) :
          theorem Polynomial.eval₂_pow {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (n : ) :
          theorem Polynomial.eval₂_dvd {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) :
          theorem Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (h : p q) (h0 : Polynomial.eval₂ f x p = 0) :
          def Polynomial.eval {R : Type u} [Semiring R] :
          RPolynomial RR

          eval x p is the evaluation of the polynomial p at x

          Instances For
            theorem Polynomial.eval_eq_sum {R : Type u} [Semiring R] {p : Polynomial R} {x : R} :
            Polynomial.eval x p = Polynomial.sum p fun e a => a * x ^ e
            theorem Polynomial.eval_eq_sum_range' {R : Type u} [Semiring R] {p : Polynomial R} {n : } (hn : Polynomial.natDegree p < n) (x : R) :
            @[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)
            @[simp]
            theorem Polynomial.eval₂_at_one {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) :
            @[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)
            @[simp]
            theorem Polynomial.eval₂_at_ofNat {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ) [Nat.AtLeastTwo n] :
            @[simp]
            theorem Polynomial.eval_C {R : Type u} {a : R} [Semiring R] {x : R} :
            Polynomial.eval x (Polynomial.C a) = a
            @[simp]
            theorem Polynomial.eval_nat_cast {R : Type u} [Semiring R] {x : R} {n : } :
            Polynomial.eval x n = n
            @[simp]
            @[simp]
            theorem Polynomial.eval_X {R : Type u} [Semiring R] {x : R} :
            Polynomial.eval x Polynomial.X = x
            @[simp]
            theorem Polynomial.eval_monomial {R : Type u} [Semiring R] {x : R} {n : } {a : R} :
            @[simp]
            theorem Polynomial.eval_zero {R : Type u} [Semiring R] {x : R} :
            @[simp]
            theorem Polynomial.eval_add {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {x : R} :
            @[simp]
            theorem Polynomial.eval_one {R : Type u} [Semiring R] {x : R} :
            @[simp]
            theorem Polynomial.eval_bit0 {R : Type u} [Semiring R] {p : Polynomial R} {x : R} :
            @[simp]
            theorem Polynomial.eval_bit1 {R : Type u} [Semiring R] {p : Polynomial R} {x : R} :
            @[simp]
            theorem Polynomial.eval_smul {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (x : R) :
            @[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
            theorem Polynomial.eval_monomial_one_add_sub {S : Type v} [CommRing S] (d : ) (y : S) :
            Polynomial.eval (1 + y) (↑(Polynomial.monomial d) (d + 1)) - Polynomial.eval y (↑(Polynomial.monomial d) (d + 1)) = Finset.sum (Finset.range (d + 1)) fun x_1 => ↑(Nat.choose (d + 1) 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}.$$

            @[simp]
            theorem Polynomial.leval_apply {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) :
            def Polynomial.leval {R : Type u_1} [Semiring R] (r : R) :

            Polynomial.eval as linear map

            Instances For
              @[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
              @[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
              @[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
              theorem Polynomial.eval_sum {R : Type u} [Semiring R] (p : Polynomial R) (f : RPolynomial R) (x : R) :
              theorem Polynomial.eval_finset_sum {R : Type u} {ι : Type y} [Semiring R] (s : Finset ι) (g : ιPolynomial R) (x : R) :
              Polynomial.eval x (Finset.sum s fun i => g i) = Finset.sum s fun i => Polynomial.eval x (g i)
              def Polynomial.IsRoot {R : Type u} [Semiring R] (p : Polynomial R) (a : R) :

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

              Instances For
                @[simp]
                theorem Polynomial.IsRoot.def {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
                theorem Polynomial.IsRoot.eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : R} (h : Polynomial.IsRoot p x) :
                theorem Polynomial.IsRoot.dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {x : R} (h : Polynomial.IsRoot p x) (hpq : p q) :
                theorem Polynomial.not_isRoot_C {R : Type u} [Semiring R] (r : R) (a : R) (hr : r 0) :
                ¬Polynomial.IsRoot (Polynomial.C r) a
                def Polynomial.comp {R : Type u} [Semiring R] (p : Polynomial R) (q : Polynomial R) :

                The composition of polynomials as a polynomial.

                Instances For
                  theorem Polynomial.comp_eq_sum_left {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
                  Polynomial.comp p q = Polynomial.sum p fun e a => Polynomial.C a * q ^ e
                  @[simp]
                  theorem Polynomial.comp_X {R : Type u} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp p Polynomial.X = p
                  @[simp]
                  theorem Polynomial.X_comp {R : Type u} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp Polynomial.X p = p
                  @[simp]
                  theorem Polynomial.comp_C {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp p (Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
                  @[simp]
                  theorem Polynomial.C_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp (Polynomial.C a) p = Polynomial.C a
                  @[simp]
                  theorem Polynomial.nat_cast_comp {R : Type u} [Semiring R] {p : Polynomial R} {n : } :
                  Polynomial.comp (n) p = n
                  @[simp]
                  theorem Polynomial.ofNat_comp {R : Type u} [Semiring R] {p : Polynomial R} (n : ) [Nat.AtLeastTwo n] :
                  @[simp]
                  theorem Polynomial.comp_zero {R : Type u} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp p 0 = Polynomial.C (Polynomial.eval 0 p)
                  @[simp]
                  theorem Polynomial.zero_comp {R : Type u} [Semiring R] {p : Polynomial R} :
                  @[simp]
                  theorem Polynomial.comp_one {R : Type u} [Semiring R] {p : Polynomial R} :
                  Polynomial.comp p 1 = Polynomial.C (Polynomial.eval 1 p)
                  @[simp]
                  theorem Polynomial.one_comp {R : Type u} [Semiring R] {p : Polynomial R} :
                  @[simp]
                  @[simp]
                  theorem Polynomial.monomial_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ) :
                  Polynomial.comp (↑(Polynomial.monomial n) a) p = Polynomial.C a * p ^ n
                  @[simp]
                  theorem Polynomial.mul_X_comp {R : Type u} [Semiring R] {p : Polynomial R} {r : Polynomial R} :
                  Polynomial.comp (p * Polynomial.X) r = Polynomial.comp p r * r
                  @[simp]
                  theorem Polynomial.X_pow_comp {R : Type u} [Semiring R] {p : Polynomial R} {k : } :
                  Polynomial.comp (Polynomial.X ^ k) p = p ^ k
                  @[simp]
                  theorem Polynomial.mul_X_pow_comp {R : Type u} [Semiring R] {p : Polynomial R} {r : Polynomial R} {k : } :
                  Polynomial.comp (p * Polynomial.X ^ k) r = Polynomial.comp p r * r ^ k
                  @[simp]
                  theorem Polynomial.C_mul_comp {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {r : Polynomial R} :
                  Polynomial.comp (Polynomial.C a * p) r = Polynomial.C a * Polynomial.comp p r
                  @[simp]
                  theorem Polynomial.nat_cast_mul_comp {R : Type u} [Semiring R] {p : Polynomial R} {r : Polynomial R} {n : } :
                  Polynomial.comp (n * p) r = n * Polynomial.comp p r
                  theorem Polynomial.mul_X_add_nat_cast_comp {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : } :
                  Polynomial.comp (p * (Polynomial.X + n)) q = Polynomial.comp p q * (q + n)
                  @[simp]
                  @[simp]
                  theorem Polynomial.pow_comp {R : Type u_1} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (n : ) :
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem Polynomial.smul_comp {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (q : Polynomial R) :
                  def Polynomial.map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :

                  map f p maps a polynomial p across a ring hom f

                  Instances For
                    @[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)
                    @[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
                    @[simp]
                    theorem Polynomial.map_monomial {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {n : } {a : R} :
                    @[simp]
                    theorem Polynomial.map_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
                    @[simp]
                    theorem Polynomial.map_add {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [Semiring S] (f : R →+* S) :
                    @[simp]
                    theorem Polynomial.map_one {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
                    @[simp]
                    theorem Polynomial.map_mul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} {q : Polynomial R} [Semiring S] (f : R →+* S) :
                    @[simp]
                    theorem Polynomial.map_smul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (r : R) :
                    def Polynomial.mapRingHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :

                    Polynomial.map as a RingHom.

                    Instances For
                      @[simp]
                      theorem Polynomial.coe_mapRingHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
                      @[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
                      @[simp]
                      theorem Polynomial.map_ofNat {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ) [Nat.AtLeastTwo n] :
                      @[simp]
                      theorem Polynomial.map_bit0 {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) :
                      @[simp]
                      theorem Polynomial.map_bit1 {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) :
                      theorem Polynomial.map_dvd {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {x : Polynomial R} {y : Polynomial R} :
                      @[simp]
                      theorem Polynomial.coeff_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ) :
                      @[simp]
                      theorem Polynomial.mapEquiv_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial R) :
                      @[simp]
                      def Polynomial.mapEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) :

                      If R and S are isomorphic, then so are their polynomial rings.

                      Instances For
                        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) :
                        @[simp]
                        theorem Polynomial.map_id {R : Type u} [Semiring R] {p : Polynomial R} :
                        theorem Polynomial.eval₂_eq_eval_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) {x : S} :
                        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) :
                        theorem Polynomial.map_monic_eq_zero_iff {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hp : Polynomial.Monic p) :
                        Polynomial.map f p = 0 ∀ (x : R), f x = 0
                        theorem Polynomial.map_monic_ne_zero {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hp : Polynomial.Monic p) [Nontrivial S] :
                        @[simp]
                        theorem Polynomial.map_pow {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ) :
                        theorem Polynomial.mem_map_range {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {p : Polynomial S} :
                        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) :
                        theorem Polynomial.eval_map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
                        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 (Finset.sum s fun i => g i) = Finset.sum s fun i => Polynomial.map f (g i)
                        @[simp]
                        theorem Polynomial.eval_zero_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) :
                        @[simp]
                        theorem Polynomial.eval_one_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) :
                        @[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)
                        @[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?

                        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₂ (RingHom.comp g 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)
                        @[simp]
                        @[simp]
                        theorem Polynomial.eval_mul {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {x : R} :

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

                        Instances For
                          theorem Polynomial.evalRingHom_zero :
                          Polynomial.evalRingHom 0 = Polynomial.constantCoeff
                          @[simp]
                          theorem Polynomial.eval_pow {R : Type u} [CommSemiring R] {p : Polynomial R} {x : R} (n : ) :

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

                          Instances For
                            theorem Polynomial.eval₂_finset_prod {R : Type u} {S : Type v} {ι : Type y} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Finset ι) (g : ιPolynomial R) (x : S) :
                            Polynomial.eval₂ f x (Finset.prod s fun i => g i) = Finset.prod s fun i => Polynomial.eval₂ f x (g i)

                            Polynomial evaluation commutes with List.prod

                            theorem Polynomial.eval_prod {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (x : R) :
                            Polynomial.eval x (Finset.prod s fun j => p j) = Finset.prod s fun j => Polynomial.eval x (p j)

                            Polynomial evaluation commutes with Finset.prod

                            theorem Polynomial.prod_comp {R : Type u} [CommSemiring R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (q : Polynomial R) :
                            Polynomial.comp (Finset.prod s fun j => p j) q = Finset.prod s fun j => Polynomial.comp (p j) q
                            theorem Polynomial.isRoot_prod {R : Type u_2} [CommRing R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ιPolynomial R) (x : R) :
                            Polynomial.IsRoot (Finset.prod s fun j => p j) x i, i s Polynomial.IsRoot (p i) x
                            theorem Polynomial.eval_dvd {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {x : R} :
                            @[simp]
                            theorem Polynomial.eval_geom_sum {R : Type u_1} [CommSemiring R] {n : } {x : R} :
                            Polynomial.eval x (Finset.sum (Finset.range n) fun i => Polynomial.X ^ i) = Finset.sum (Finset.range n) fun i => x ^ i
                            theorem Polynomial.map_prod {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) {ι : Type u_1} (g : ιPolynomial R) (s : Finset ι) :
                            Polynomial.map f (Finset.prod s fun i => g i) = Finset.prod s fun i => Polynomial.map f (g i)
                            theorem Polynomial.IsRoot.map {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R} (h : Polynomial.IsRoot p 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.IsRoot (Polynomial.map f p) (f x)) (hf : Function.Injective f) :
                            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) :
                            theorem Polynomial.C_neg {R : Type u} {a : R} [Ring R] :
                            Polynomial.C (-a) = -Polynomial.C a
                            theorem Polynomial.C_sub {R : Type u} {a : R} {b : R} [Ring R] :
                            Polynomial.C (a - b) = Polynomial.C a - Polynomial.C b
                            @[simp]
                            theorem Polynomial.map_sub {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) :
                            @[simp]
                            theorem Polynomial.map_neg {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) :
                            @[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
                            @[simp]
                            theorem Polynomial.eval_int_cast {R : Type u} [Ring R] {n : } {x : R} :
                            Polynomial.eval x n = n
                            @[simp]
                            theorem Polynomial.eval₂_neg {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) {x : S} :
                            @[simp]
                            theorem Polynomial.eval₂_sub {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) {x : S} :
                            @[simp]
                            theorem Polynomial.eval_neg {R : Type u} [Ring R] (p : Polynomial R) (x : R) :
                            @[simp]
                            theorem Polynomial.eval_sub {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) (x : R) :
                            theorem Polynomial.root_X_sub_C {R : Type u} {a : R} {b : R} [Ring R] :
                            Polynomial.IsRoot (Polynomial.X - Polynomial.C a) b a = b
                            @[simp]
                            theorem Polynomial.neg_comp {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} :
                            @[simp]
                            theorem Polynomial.sub_comp {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {r : Polynomial R} :
                            @[simp]
                            theorem Polynomial.cast_int_comp {R : Type u} [Ring R] {p : Polynomial R} (i : ) :
                            Polynomial.comp (i) p = i
                            @[simp]
                            theorem Polynomial.eval₂_at_int_cast {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) (n : ) :
                            Polynomial.eval₂ f (n) p = f (Polynomial.eval (n) p)
                            theorem Polynomial.mul_X_sub_int_cast_comp {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} {n : } :
                            Polynomial.comp (p * (Polynomial.X - n)) q = Polynomial.comp p q * (q - n)