:: deftheorem Def8 defines KroneckerIso FIELD_4:def 9 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for b₃ being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) holds
( b₃ = KroneckerIso p iff for q being Element of the carrier of (Polynom-Ring p) holds b₃ . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) );