:: deftheorem Def7 defines multiplicity UPROOTS:def 8 :
for L being non degenerated comRing
for x being Element of L
for p being non-zero Polynomial of L
for b₄ being Element of NAT holds
( b₄ = multiplicity (p,x) iff ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } & b₄ = max F ) );