no goals
R : Type u_1
A : Type u_3
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ ↑(aeval x) (map (algebraMap R A) p) = ↑(aeval x) p
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]