theorem :: FIELD_13:57

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( FAdj (F,{a}) is F -normal iff MinPoly (a,F) splits_in FAdj (F,{a}) )