:: deftheorem defines is_integral_over ALGNUM_1:def 2 :
for A, B being Ring
for x being Element of B holds
( x is_integral_over A iff ex f being Polynomial of A st
( LC f = 1. A & Ext_eval (f,x) = 0. B ) );