theorem multi4: :: FIELD_15:70

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of F st a is_a_root_of p holds
( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) )