let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E st not a in F holds
for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E st not a in F holds
for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b
let a be F -algebraic Element of E; :: thesis: ( not a in F implies for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b )
assume AS1: not a in F ; :: thesis: for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b
let b be Element of F; :: thesis: ( b = a ^2 implies MinPoly (a,F) = X^2- b )
assume AS2: b = a ^2 ; :: thesis: MinPoly (a,F) = X^2- b
set p = X^2- b;
B: ( X^2- b is monic & deg (X^2- b) = 2 ) by FIELD_9:def 4;
C: Ext_eval ((X^2- b),a) = 0. E by AS2, lemBas00;
for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg (X^2- b) <= deg q by B, AS1, lemBas01;
hence MinPoly (a,F) = X^2- b by C, FIELD_6:51; :: thesis: verum