let F be Field; :: thesis: 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 ) )
let p be non zero Polynomial of F; :: thesis: 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 ) )
let a be Element of F; :: thesis: for n being Element of NAT holds
( n = multiplicity (p,a) iff ( (X- a) `^ n divides p & not (X- a) `^ (n + 1) divides p ) )
let n be Element of NAT ; :: thesis: ( n = multiplicity (p,a) iff ( (X- a) `^ n divides p & not (X- a) `^ (n + 1) divides p ) )
rpoly (1,a) = X- a by FIELD_9:def 2;
hence ( n = multiplicity (p,a) iff ( (X- a) `^ n divides p & not (X- a) `^ (n + 1) divides p ) ) by RING_5:33; :: thesis: verum