:: deftheorem defines algebraic_integer ALGNUM_1:def 6 :
for c being Complex holds
( c is algebraic_integer iff ex x being Element of F_Complex st
( x = c & x is_integral_over INT.Ring ) );