:: deftheorem dpf defines perfect FIELD_15:def 4 :
for F being Field holds
( F is perfect iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds p is separable );