Algebra over the Ring of Polynomials

@[simp]

theorem Polynomial.eval₂_id {R : Type u_1} [CommSemiring R] {p : Polynomial R} {x : R} : eval₂ (RingHom.id R) x p = eval x p

instance Polynomial.instAlgebraPi {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra (Polynomial R) (S → S)

Equations

• Polynomial.instAlgebraPi = (Pi.ringHom fun (x : S) => (Polynomial.aeval x).toRingHom).toAlgebra

@[simp]

theorem Polynomial.aeval_polynomial_pi {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (p : Polynomial (Polynomial R)) (f : S → S) (x : S) : (aeval f) p x = (aevalAeval x (f x)) p

#TODO: Generalize the following lemma to CommSemiring.