let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) ex E being F -finite FieldExtension of F st
( p is_with_roots_in E & deg (E,F) <= deg p )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being F -finite FieldExtension of F st
( p is_with_roots_in E & deg (E,F) <= deg p )
consider q being Element of (Polynom-Ring F) such that
A: q is_a_irreducible_factor_of p by FIELD_1:3;
reconsider q = q as Element of the carrier of (Polynom-Ring F) ;
consider E being F -finite FieldExtension of F such that
C: ( deg (E,F) = deg q & q is_with_roots_in E ) by A, mi2;
take E ; :: thesis: ( p is_with_roots_in E & deg (E,F) <= deg p )
reconsider p1 = p, q1 = q as Polynomial of F ;
q1 divides p1 by A;
then consider r1 being Polynomial of F such that
D: q1 *' r1 = p1 by RING_4:1;
consider a being Element of E such that
E: a is_a_root_of q,E by C, FIELD_4:def 3;
F is Subring of E by FIELD_4:def 1;
then Ext_eval (p1,a) = (Ext_eval (q1,a)) * (Ext_eval (r1,a)) by D, ALGNUM_1:20
.= (0. E) * (Ext_eval (r1,a)) by E, FIELD_4:def 2 ;
hence p is_with_roots_in E by FIELD_4:def 3, FIELD_4:def 2; :: thesis: deg (E,F) <= deg p
q1 divides p1 by A;
hence deg (E,F) <= deg p by C, RING_5:13; :: thesis: verum