theorem uu4: :: FIELD_8:15

for F being Field
for E being FieldExtension of F
for a being b₁ -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