let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q )
let p be non constant Element of the carrier of (Polynom-Ring F); ( p is separable iff for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q )
A:
now ( p is separable implies for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q )assume AS:
p is
separable
;
for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * qthus
for
E being
SplittingField of
p ex
a being
Element of
E ex
q being
Ppoly of
E,
(Roots (E,p)) st
p = a * q
verumproof
let E be
SplittingField of
p;
ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q
A:
p splits_in E
by FIELD_8:def 1;
then consider c being non
zero Element of
E,
q being
Ppoly of
E such that B:
p = c * q
by FIELD_4:def 5;
H:
Roots (
E,
p)
= { a where a is Element of E : a is_a_root_of p,E }
by FIELD_4:def 4;
I:
c * q is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
C:
Roots q =
Roots (c * q)
by RING_5:19
.=
Roots (
E,
p)
by I, B, FIELD_7:13
;
now for a being Element of E st a is_a_root_of q holds
multiplicity (q,a) = 1let a be
Element of
E;
( a is_a_root_of q implies multiplicity (q,a) = 1 )assume
a is_a_root_of q
;
multiplicity (q,a) = 1then
a in Roots (
E,
p)
by C, POLYNOM5:def 10;
then consider a1 being
Element of
E such that D:
(
a1 = a &
a1 is_a_root_of p,
E )
by H;
multiplicity (
p,
a)
= 1
by D, A, AS, ThSep0;
then
multiplicity (
(c * q),
a)
= 1
by B, sepsep1;
hence
multiplicity (
q,
a)
= 1
by lems;
verum end;
then
q is
Ppoly of
E,
(Roots q)
by FIELD_14:30;
hence
ex
a being
Element of
E ex
q being
Ppoly of
E,
(Roots (E,p)) st
p = a * q
by C, B;
verum
end; end;
now ( ( for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q ) implies p is separable )assume AS:
for
E being
SplittingField of
p ex
a being
Element of
E ex
q being
Ppoly of
E,
(Roots (E,p)) st
p = a * q
;
p is separable set K = the
SplittingField of
p;
consider c being
Element of the
SplittingField of
p,
q being
Ppoly of the
SplittingField of
p,
(Roots ( the SplittingField of p,p)) such that A:
p = c * q
by AS;
(0. the SplittingField of p) * q =
0_. the
SplittingField of
p
by POLYNOM5:26
.=
0_. F
by FIELD_4:12
;
then reconsider c =
c as non
zero Element of the
SplittingField of
p by A, STRUCT_0:def 12;
H:
Roots ( the
SplittingField of
p,
p)
= { a where a is Element of the SplittingField of p : a is_a_root_of p, the SplittingField of p }
by FIELD_4:def 4;
I:
c * q is
Element of the
carrier of
(Polynom-Ring the SplittingField of p)
by POLYNOM3:def 10;
C:
Roots q =
Roots (c * q)
by RING_5:19
.=
Roots ( the
SplittingField of
p,
p)
by I, A, FIELD_7:13
;
now for a being Element of the SplittingField of p st a is_a_root_of p, the SplittingField of p holds
multiplicity (p,a) = 1let a be
Element of the
SplittingField of
p;
( a is_a_root_of p, the SplittingField of p implies multiplicity (p,a) = 1 )assume
a is_a_root_of p, the
SplittingField of
p
;
multiplicity (p,a) = 1then
a in Roots ( the
SplittingField of
p,
p)
by H;
then
a is_a_root_of q
by C, POLYNOM5:def 10;
then
multiplicity (
q,
a)
= 1
by C, FIELD_14:30;
then
multiplicity (
(c * q),
a)
= 1
by lems;
hence
multiplicity (
p,
a)
= 1
by A, sepsep1;
verum end; hence
p is
separable
;
verum end;
hence
( p is separable iff for E being SplittingField of p ex a being Element of E ex q being Ppoly of E,(Roots (E,p)) st p = a * q )
by A; verum