∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
  (Polynomial.aeval (AdjoinRoot.root (minpoly R pb.gen))) (minpoly R pb.gen) = 0