theorem multi2: :: FIELD_14:67

for F being Field
for p being non zero Polynomial of F
for a being Element of F
for n being Element of NAT holds
( n = multiplicity (p,a) iff ( (X- a) `^ n divides p & not (X- a) `^ (n + 1) divides p ) )