:: deftheorem defines emb FIELD_1:def 4 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds emb p = (canHom ({p} -Ideal)) * (canHom F);