:: deftheorem defines KroneckerField FIELD_1:def 3 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal);