feat(Algebra/Polynomial/AlgebraMap): add Polynomial.aeval_eq_aeval_map (leanprover-community#34788)

This lemma is a special case of `Polynomial.map_aeval_eq_aeval_map` when `U = T` and `ψ` the identity.

Author: justus-springer

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -493,6 +493,11 @@ theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Se
   conv_rhs => rw [← eval_map_algebraMap]
   rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
 
+theorem aeval_eq_aeval_map [Semiring S] [CommSemiring T] [Algebra R S]
+    [Algebra T S] {φ : R →+* T} (h : (algebraMap T S).comp φ = (algebraMap R S))
+    (p : R[X]) (a : S) : aeval a p = aeval a (p.map φ) :=
+  map_aeval_eq_aeval_map (by rwa [RingHom.id_comp]) p a
+
 theorem aeval_eq_zero_of_dvd_aeval_eq_zero [CommSemiring S] [CommSemiring T] [Algebra S T]
     {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0 := by
   rw [← eval_map_algebraMap] at h₂ ⊢