:: deftheorem defines Ann_Poly ALGNUM_1:def 8 :
for A, B being Ring
for x being Element of B holds Ann_Poly (x,A) = { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;