let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for p being irreducible Element of the carrier of (Polynom-Ring F) st Ext_eval (p,a) = 0. E holds
MinPoly (a,F) = NormPolynomial p
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for p being irreducible Element of the carrier of (Polynom-Ring F) st Ext_eval (p,a) = 0. E holds
MinPoly (a,F) = NormPolynomial p
let a be F -algebraic Element of E; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) st Ext_eval (p,a) = 0. E holds
MinPoly (a,F) = NormPolynomial p
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ( Ext_eval (p,a) = 0. E implies MinPoly (a,F) = NormPolynomial p )
set q = NormPolynomial p;
assume Ext_eval (p,a) = 0. E ; :: thesis: MinPoly (a,F) = NormPolynomial p
then Ext_eval ((NormPolynomial p),a) = 0. E by FIELD_6:25;
hence MinPoly (a,F) = NormPolynomial p by RING_4:28, FIELD_6:52; :: thesis: verum