no goals
R : Type u
S : Type ?u.133744
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : ↑(aeval a) p = 0
⊢ ↑(aeval (↑f a)) p = 0
rw [aeval_algHom, f.comp_apply, ha, map_zero]