:: deftheorem defines KrRootP FIELD_5:def 3 :
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRootP p = (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);