let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being F -finite FieldExtension of F st
( deg (E,F) = deg p & p is_with_roots_in E )
let p1 be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ex E being F -finite FieldExtension of F st
( deg (E,F) = deg p1 & p1 is_with_roots_in E )
set p = NormPolynomial p1;
consider E being FieldExtension of F, a being F -algebraic Element of E such that
A: NormPolynomial p1 = MinPoly (a,F) by mi1, RING_4:28;
reconsider L = FAdj (F,{a}) as F -finite FieldExtension of F ;
take L ; :: thesis: ( deg (L,F) = deg p1 & p1 is_with_roots_in L )
not p1 is constant ;
then (len p1) - 1 > 0 by HURWITZ:def 2;
then B: len p1 <> 0 ;
deg (NormPolynomial p1) = (len (NormPolynomial p1)) - 1 by HURWITZ:def 2
.= (len p1) - 1 by B, POLYNOM5:57
.= deg p1 by HURWITZ:def 2 ;
hence deg (L,F) = deg p1 by A, FIELD_6:67; :: thesis: p1 is_with_roots_in L
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of L ;
L is Subring of E by FIELD_5:12;
then reconsider E = E as L -extending FieldExtension of F by FIELD_4:def 1;
for a being Element of E
for b being Element of L st a = b holds
Ext_eval ((NormPolynomial p1),a) = Ext_eval ((NormPolynomial p1),b) by FIELD_7:14;
then Ext_eval ((NormPolynomial p1),a1) = Ext_eval ((NormPolynomial p1),a)
.= 0. E by A, FIELD_6:52
.= 0. L by EC_PF_1:def 1 ;
then Ext_eval (p1,a1) = 0. L by FIELD_6:25;
hence p1 is_with_roots_in L by FIELD_4:def 3, FIELD_4:def 2; :: thesis: verum