let F be Field; :: thesis: for E being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) )
let E be FieldExtension of F; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) )
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring E) ;
reconsider q = q as Polynomial of E ;
H: ( deg p > 0 & deg q = deg p ) by RING_4:def 4, FIELD_4:20;
then reconsider q = q as non constant Polynomial of E by RATFUNC1:def 2;

A: now :: thesis: ( card (Roots (E,p)) = deg p implies ( p splits_in E & p is separable ) )

assume B: card (Roots (E,p)) = deg p ; :: thesis: ( p splits_in E & p is separable )
Roots q = Roots (E,p) by FIELD_7:13;
then consider x being non zero Element of E, v being Ppoly of E such that
C: q = x * v by H, B, FIELD_15:69, FIELD_4:def 5;
thus ( p splits_in E & p is separable ) by B, C, FIELD_4:def 5, FIELD_15:85; :: thesis: verum

end;

now :: thesis: ( p splits_in E & p is separable implies deg p = card (Roots (E,p)) )

assume AS: ( p splits_in E & p is separable ) ; :: thesis: deg p = card (Roots (E,p))
consider x being non zero Element of E, v being Ppoly of E such that
A: p = x * v by AS, FIELD_4:def 5;

now :: thesis: for a being Element of E holds multiplicity (q,a) <= 1

let a be Element of E; :: thesis: multiplicity (q,b₁) <= 1

per cases ( not a is_a_root_of p,E or a is_a_root_of p,E ) ;

suppose C: not a is_a_root_of p,E ; :: thesis: multiplicity (q,b₁) <= 1

now :: thesis: not a is_a_root_of q

assume a is_a_root_of q ; :: thesis: contradiction
then 0. E = Ext_eval (p,a) by FIELD_4:26;
hence contradiction by C, FIELD_4:def 2; :: thesis: verum

end;

hence multiplicity (q,a) <= 1 by UPROOTS:52; :: thesis: verum

end;

suppose a is_a_root_of p,E ; :: thesis: multiplicity (q,b₁) <= 1

then multiplicity (p,a) = 1 by AS, FIELD_15:75;
hence multiplicity (q,a) <= 1 by FIELD_14:def 6; :: thesis: verum

end;

end;

end;

hence deg p = card (Roots q) by H, A, FIELD_4:def 5, FIELD_15:69
.= card (Roots (E,p)) by FIELD_7:13 ;
:: thesis: verum

end;

hence ( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) ) by A; :: thesis: verum