no goals
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Type ?u.52206
inst✝⁵ : CommRing P
inst✝⁴ : IsLocalization M S
R' : Type u_2
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : ↑(aeval x) p = 0
⊢ ↑(aeval x) (integerNormalization M p) = 0
rw [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero _ _ _ hx]