eval2 for alg_homs

Stream: Is there code for X?

[Chris Hughes]

I'm looking for something like this, for defining an alg_hom out of a polynomial ring, polynomial S, but it's only an alg_hom over a smaller ring than S.

example {R S A : Type} [comm_ring R] [comm_ring S] [comm_ring A]
  [algebra R A] [algebra R S] (f : S →ₐ[R] A) (x : A) : polynomial S →ₐ[R] A :=
sorry

Motivation : to define mv_polynomial.option_equiv_left in such a way that I actually know what it does to elements.

[Anne Baanen]

Is docs#polynomial.aeval too specific here? Edit: yes

[Eric Wieser]

Does the version for add_monoid_algebra exist?