theorem :: FIELD_1:45

for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) st not p is with_roots holds
not emb p is isomorphism by Th45;