theorem mulzero1: :: FIELD_15:56

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
( (X- a) `^ n divides p iff multiplicity (p,a) >= n )