theorem mpol2: :: FIELD_6:51

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg p <= deg q ) ) )