:: deftheorem defines -algebraic FIELD_6:def 7 :
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ker (hom_Ext_eval (a,F)) <> {(0. (Polynom-Ring F))} );