for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )