no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a : AdjoinRoot (minpoly R x)
⊢ ↑(aeval { val := x, property := (_ : x ∈ adjoin R {x}) }) (minpoly R x) = 0
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]