no goals
R : Type u_3
A : Type u_1
B : Type u_2
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
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ ↑(aeval (↑(algebraMap A B) x)) p = 0 ↔ ↑(aeval x) p = 0
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
  iff_false_intro (one_ne_zero' B), or_false_iff]