theorem :: FIELD_15:71

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( ex a being Element of F st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) is with_roots )