no goals
R : Type u_1
A : Type u_2
B : Type u_3
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 : A
p : R[X]
h : Function.Injective ↑(algebraMap A B)
⊢ ↑(aeval (↑(algebraMap A B) x)) p = 0 ↔ ↑(aeval x) p = 0
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]