let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being F -algebraic Element of E
for b being F -algebraic Element of K st a = b holds
MinPoly (a,F) = MinPoly (b,F)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for a being F -algebraic Element of E
for b being F -algebraic Element of K st a = b holds
MinPoly (a,F) = MinPoly (b,F)
let K be E -extending FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for b being F -algebraic Element of K st a = b holds
MinPoly (a,F) = MinPoly (b,F)
let a be F -algebraic Element of E; :: thesis: for b being F -algebraic Element of K st a = b holds
MinPoly (a,F) = MinPoly (b,F)
let b be F -algebraic Element of K; :: thesis: ( a = b implies MinPoly (a,F) = MinPoly (b,F) )
H: E is Subfield of K by FIELD_4:7;
assume a = b ; :: thesis: MinPoly (a,F) = MinPoly (b,F)
then Ext_eval ((MinPoly (a,F)),b) = Ext_eval ((MinPoly (a,F)),a) by FIELD_7:14
.= 0. E by FIELD_6:52
.= 0. K by H, EC_PF_1:def 1 ;
hence MinPoly (a,F) = MinPoly (b,F) by FIELD_6:52; :: thesis: verum