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
h : Function.Injective ↑(algebraMap S A)
x✝ : IsAlgebraic R (↑(algebraMap S A) a)
p : R[X]
hp0 : p ≠ 0
hp : ↑(aeval (↑(algebraMap S A) a)) p = 0
⊢ ↑(algebraMap S A) (↑(aeval a) p) = ↑(algebraMap S A) 0
rwa [map_zero, ← aeval_algebraMap_apply]