let F be Field; :: thesis: for E being F -finite FieldExtension of F
for a being Element of E holds deg (MinPoly (a,F)) divides deg (E,F)
let E be F -finite FieldExtension of F; :: thesis: for a being Element of E holds deg (MinPoly (a,F)) divides deg (E,F)
let a be Element of E; :: thesis: deg (MinPoly (a,F)) divides deg (E,F)
set K = FAdj (F,{a});
reconsider E1 = E as F -extending FAdj (F,{a}) -finite FieldExtension of F by FIELD_4:7, FIELD_7:31;
deg (E1,F) = (deg (E1,(FAdj (F,{a})))) * (deg ((FAdj (F,{a})),F)) by FIELD_7:30
.= (deg (E1,(FAdj (F,{a})))) * (deg (MinPoly (a,F))) by FIELD_6:67 ;
hence deg (MinPoly (a,F)) divides deg (E,F) by INT_1:def 3; :: thesis: verum