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 & p is irreducible & ker (hom_Ext_eval (a,F)) = {p} -Ideal ) )