feat(data/polynomial/algebra_map): aeval_map (#5843)

Proves `aeval_map`, which relates `aeval` within an `is_scalar_tower`.

src/data/polynomial/algebra_map.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 
 import data.polynomial.eval
+import algebra.algebra.tower
 
 /-!
 # Theory of univariate polynomials
@@ -147,6 +148,11 @@ lemma aeval_comp {A : Type*} [comm_semiring A] [algebra R A] (x : A) :
   aeval x (p.comp q) = (aeval (aeval x q) p) :=
 eval₂_comp (algebra_map R A)
 
+@[simp] lemma aeval_map {A : Type*} [comm_semiring A] [algebra R A] [algebra A B]
+  [is_scalar_tower R A B] (b : B) (p : polynomial R) :
+  aeval b (p.map (algebra_map R A)) = aeval b p :=
+by rw [aeval_def, eval₂_map, ←is_scalar_tower.algebra_map_eq, ←aeval_def]
+
 theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
   φ p = eval₂ (algebra_map R A) (φ X) p :=
 begin