no goals
R : Type u
S : Type u_1
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
a : S
x✝ : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval a) f = 0
⊢ ↑(aeval (↑(algebraMap S A) a)) f = 0
rw [aeval_algebraMap_apply, hf₂, map_zero]