let F be Field; :: thesis: for E being FieldExtension of F
for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)
let E be FieldExtension of F; :: thesis: for p being non zero Polynomial of F
for c being non zero Element of F
for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)
let p be non zero Polynomial of F; :: thesis: for c being non zero Element of F
for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)
let c be non zero Element of F; :: thesis: for a being Element of E holds multiplicity ((c * p),a) = multiplicity (p,a)
let a be Element of E; :: thesis: multiplicity ((c * p),a) = multiplicity (p,a)
set n = multiplicity (p,a);
reconsider q = p as Polynomial of E by FIELD_4:8;
p <> 0_. F ;
then p <> 0_. E by FIELD_4:12;
then reconsider q = q as non zero Polynomial of E by UPROOTS:def 5;
( F is Subfield of E & c <> 0. F ) by FIELD_4:7;
then H: ( c <> 0. E & @ (c,E) = c ) by EC_PF_1:def 1, FIELD_7:def 4;
then K: not @ (c,E) is zero ;
then reconsider cq = (@ (c,E)) * q as non zero Polynomial of E ;
I: (@ (c,E)) * q = c * p by H, ll;
multiplicity (q,a) = multiplicity (p,a) by sepsep1;
then ( (X- a) `^ (multiplicity (p,a)) divides q & not (X- a) `^ ((multiplicity (p,a)) + 1) divides q ) by FIELD_14:67;
then ( (X- a) `^ (multiplicity (p,a)) divides (@ (c,E)) * q & not (X- a) `^ ((multiplicity (p,a)) + 1) divides (@ (c,E)) * q ) by K, RING_5:15;
then multiplicity (cq,a) = multiplicity (p,a) by FIELD_14:67;
hence multiplicity ((c * p),a) = multiplicity (p,a) by I, sepsep1; :: thesis: verum