no goals
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : R
n : ℕ
⊢ ↑(algebraMap R A) (eval x (T R n)) = eval (↑(algebraMap R A) x) (T A n)
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]