let F be Field; :: thesis: for p being non zero Polynomial of F
for a being Element of F holds deg p >= multiplicity (p,a)
let p be non zero Polynomial of F; :: thesis: for a being Element of F holds deg p >= multiplicity (p,a)
let a be Element of F; :: thesis: deg p >= multiplicity (p,a)
set m = multiplicity (p,a);
( (X- a) `^ (multiplicity (p,a)) divides p & deg ((X- a) `^ (multiplicity (p,a))) = multiplicity (p,a) ) by FIELD_14:67, Lm12a;
hence deg p >= multiplicity (p,a) by RING_5:13; :: thesis: verum