theorem :: FIELD_6:59

for F being Field
for E being Polynom-Ring b₁ -homomorphic FieldExtension of F
for a being b₁ -algebraic Element of E holds (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic