let F be Field; for E being FieldExtension of F
for a being F -algebraic Element of E holds MinPoly (a,F) is irreducible
let E be FieldExtension of F; for a being F -algebraic Element of E holds MinPoly (a,F) is irreducible
let a be F -algebraic Element of E; MinPoly (a,F) is irreducible
set m = MinPoly (a,F);
X:
F is Subring of E
by FIELD_4:def 1;
a is_integral_over F
by alg1;
then Z:
( 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 )
;
reconsider m2 = MinPoly (a,F) as Element of (Polynom-Ring F) ;
reconsider m1 = m1 as non zero Element of the carrier of (Polynom-Ring F) by Z1, Z, UPROOTS:def 5;
A2:
MinPoly (a,F) <> 0. (Polynom-Ring F)
by Z, POLYNOM3:def 10;
now for x being Element of (Polynom-Ring F) holds
( not x divides MinPoly (a,F) or x is Unit of (Polynom-Ring F) or x is_associated_to MinPoly (a,F) )let x be
Element of
(Polynom-Ring F);
( not x divides MinPoly (a,F) or b1 is Unit of (Polynom-Ring F) or b1 is_associated_to MinPoly (a,F) )assume B:
x divides MinPoly (
a,
F)
;
( b1 is Unit of (Polynom-Ring F) or b1 is_associated_to MinPoly (a,F) )consider y being
Element of
(Polynom-Ring F) such that A4:
x * y = m2
by B;
reconsider x1 =
x,
y1 =
y as
Polynomial of
F by POLYNOM3:def 10;
m1 = x1 *' y1
by Z1, A4, POLYNOM3:def 10;
then A5:
Ext_eval (
m1,
a)
= (Ext_eval (x1,a)) * (Ext_eval (y1,a))
by ALGNUM_1:20, X;
per cases
( Ext_eval (x1,a) = 0. E or Ext_eval (y1,a) = 0. E )
by A5, Z1, VECTSP_2:def 1;
suppose
Ext_eval (
y1,
a)
= 0. E
;
( b1 is Unit of (Polynom-Ring F) or b1 is_associated_to MinPoly (a,F) )then
y1 in {(MinPoly (a,F))} -Ideal
by Z;
then
y1 in { ((MinPoly (a,F)) * r) where r is Element of (Polynom-Ring F) : verum }
by IDEAL_1:64;
then consider r being
Element of
(Polynom-Ring F) such that A6:
y1 = (MinPoly (a,F)) * r
;
reconsider r1 =
r as
Polynomial of
F by POLYNOM3:def 10;
A8:
x * r = x1 *' r1
by POLYNOM3:def 10;
(1. (Polynom-Ring F)) * (MinPoly (a,F)) =
x * (r * (MinPoly (a,F)))
by A6, A4, GROUP_1:def 12
.=
(x * r) * (MinPoly (a,F))
by GROUP_1:def 3
;
then
(1_. F) *' m1 = (x1 *' r1) *' m1
by Z1, A8, POLYNOM3:def 10;
then 1_. F =
x1 *' r1
by RATFUNC1:7
.=
x * r
by POLYNOM3:def 10
;
then
1. (Polynom-Ring F) = x * r
by POLYNOM3:def 10;
then
x divides 1. (Polynom-Ring F)
;
hence
(
x is
Unit of
(Polynom-Ring F) or
x is_associated_to MinPoly (
a,
F) )
by GCD_1:def 2;
verum end; end; end;
hence
MinPoly (a,F) is irreducible
by A2, A3, RING_2:def 9; verum