let F be Field; for E being FieldExtension of F
for a being F -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 & Ext_eval (p,a) = 0. E ) )
let E be FieldExtension of F; for a being F -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 & Ext_eval (p,a) = 0. E ) )
let a be F -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 & Ext_eval (p,a) = 0. E ) )
let p be Element of the carrier of (Polynom-Ring F); ( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
set m = MinPoly (a,F);
set g = hom_Ext_eval (a,F);
X:
F is Subring of E
by FIELD_4:def 1;
a is_integral_over F
by alg1;
then
( MinPoly (a,F) <> 0_. F & {(MinPoly (a,F))} -Ideal = Ann_Poly (a,F) & MinPoly (a,F) = NormPolynomial (MinPoly (a,F)) )
by X, ALGNUM_1:def 9;
then
MinPoly (a,F) in { p where p is Polynomial of F : Ext_eval (p,a) = 0. E }
by IDEAL_1:66;
then consider m1 being Polynomial of F such that
Z1:
( m1 = MinPoly (a,F) & Ext_eval (m1,a) = 0. E )
;
now ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E implies p = MinPoly (a,F) )assume A:
(
p is
monic &
p is
irreducible &
Ext_eval (
p,
a)
= 0. E )
;
p = MinPoly (a,F)reconsider p1 =
p as
Element of
(Polynom-Ring F) ;
ker (hom_Ext_eval (a,F)) is
principal
by IDEAL_1:def 28;
then consider u being
Element of
(Polynom-Ring F) such that C1:
ker (hom_Ext_eval (a,F)) = {u} -Ideal
;
(hom_Ext_eval (a,F)) . p = 0. E
by A, ALGNUM_1:def 11;
then
p in { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E }
;
then C2:
p in {u} -Ideal
by C1, VECTSP10:def 9;
p in { (u * r) where r is Element of (Polynom-Ring F) : verum }
by C2, IDEAL_1:64;
then consider v being
Element of
(Polynom-Ring F) such that C3:
p = u * v
;
reconsider u1 =
u as
Polynomial of
F by POLYNOM3:def 10;
u divides p
by C3;
then
u is_associated_to p
by A2, A, RING_2:def 9;
then
{p} -Ideal = ker (hom_Ext_eval (a,F))
by C1, RING_2:21;
hence
p = MinPoly (
a,
F)
by A, mpol1;
verum end;
hence
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
by Z1; verum