let F be Field; :: thesis: for p being non zero Polynomial of F
for a being Element of F holds multiplicity ((NormPolynomial p),a) = multiplicity (p,a)
let p be non zero Polynomial of F; :: thesis: for a being Element of F holds multiplicity ((NormPolynomial p),a) = multiplicity (p,a)
let a be Element of F; :: thesis: multiplicity ((NormPolynomial p),a) = multiplicity (p,a)
set n = multiplicity (p,a);
A: ( (X- a) `^ (multiplicity (p,a)) divides p & not (X- a) `^ ((multiplicity (p,a)) + 1) divides p ) by FIELD_14:67;
( p is Element of the carrier of (Polynom-Ring F) & (X- a) `^ (multiplicity (p,a)) is Element of the carrier of (Polynom-Ring F) & (X- a) `^ ((multiplicity (p,a)) + 1) is Element of the carrier of (Polynom-Ring F) & NormPolynomial p is Element of the carrier of (Polynom-Ring F) ) by POLYNOM3:def 10;
then ( (X- a) `^ (multiplicity (p,a)) divides NormPolynomial p & not (X- a) `^ ((multiplicity (p,a)) + 1) divides NormPolynomial p ) by A, RING_4:26;
hence multiplicity ((NormPolynomial p),a) = multiplicity (p,a) by FIELD_14:67; :: thesis: verum