:: deftheorem defines KroneckerField FIELD_11:def 9 :
for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal holds KroneckerField (F,g,I) = (Polynom-Ring ((card (nonConstantPolys F)),F)) / I;