:: deftheorem Def7 defines minimal_polynom ALGNUM_1:def 9 :
for K, L being Field
for z being Element of L st K is Subring of L & z is_integral_over K holds
for b₄ being Element of the carrier of (Polynom-Ring K) holds
( b₄ = minimal_polynom (z,K) iff ( b₄ <> 0_. K & {b₄} -Ideal = Ann_Poly (z,K) & b₄ = NormPolynomial b₄ ) );