let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f is_with_roots_in E

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f is_with_roots_in E

consider p being Element of the carrier of (Polynom-Ring F) such that

A: p is_a_irreducible_factor_of f by FIELD_1:3;

reconsider p = p as irreducible Element of the carrier of (Polynom-Ring F) by A;

consider q being Element of the carrier of (Polynom-Ring F) such that

B: p * q = f by A, GCD_1:def 1;

consider E being FieldExtension of F such that

C: p is_with_roots_in E by kron;

take E ; :: thesis: f is_with_roots_in E

consider a being Element of E such that

D: a is_a_root_of p,E by C, FIELD_4:def 3;

reconsider p1 = p, q1 = q as Polynomial of F ;

F: F is Subring of E by FIELD_4:def 1;

Ext_eval (f,a) = Ext_eval ((p1 *' q1),a) by B, POLYNOM3:def 10

.= (Ext_eval (p1,a)) * (Ext_eval (q1,a)) by F, ALGNUM_1:20

.= (0. E) * (Ext_eval (q1,a)) by D, FIELD_4:def 2 ;

hence f is_with_roots_in E by FIELD_4:def 2, FIELD_4:def 3; :: thesis: verum

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f is_with_roots_in E

consider p being Element of the carrier of (Polynom-Ring F) such that

A: p is_a_irreducible_factor_of f by FIELD_1:3;

reconsider p = p as irreducible Element of the carrier of (Polynom-Ring F) by A;

consider q being Element of the carrier of (Polynom-Ring F) such that

B: p * q = f by A, GCD_1:def 1;

consider E being FieldExtension of F such that

C: p is_with_roots_in E by kron;

take E ; :: thesis: f is_with_roots_in E

consider a being Element of E such that

D: a is_a_root_of p,E by C, FIELD_4:def 3;

reconsider p1 = p, q1 = q as Polynomial of F ;

F: F is Subring of E by FIELD_4:def 1;

Ext_eval (f,a) = Ext_eval ((p1 *' q1),a) by B, POLYNOM3:def 10

.= (Ext_eval (p1,a)) * (Ext_eval (q1,a)) by F, ALGNUM_1:20

.= (0. E) * (Ext_eval (q1,a)) by D, FIELD_4:def 2 ;

hence f is_with_roots_in E by FIELD_4:def 2, FIELD_4:def 3; :: thesis: verum