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 FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )
let p be non constant Element of the carrier of (Polynom-Ring F); ( p is separable iff for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )
A:
now ( p is separable implies for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )assume AS:
p is
separable
;
for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1now for E being FieldExtension of F
for a being Element of E holds not multiplicity (p,a) > 1let E be
FieldExtension of
F;
for a being Element of E holds not multiplicity (p,a) > 1let a be
Element of
E;
not multiplicity (p,a) > 1assume B:
multiplicity (
p,
a)
> 1
;
contradiction
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider p1 =
p as
Element of the
carrier of
(Polynom-Ring E) ;
deg p > 0
by RING_4:def 4;
then
deg p1 > 0
by FIELD_4:20;
then reconsider p1 =
p1 as non
constant Element of the
carrier of
(Polynom-Ring E) by RING_4:def 4;
consider K being
FieldExtension of
E such that D:
p1 splits_in K
by FIELD_5:31;
reconsider K =
K as
E -extending FieldExtension of
F ;
multiplicity (
p1,
a)
> 1
by B, FIELD_14:def 6;
then
multiplicity (
p1,
(@ (a,K)))
> 1
by multi3;
then E:
multiplicity (
p,
(@ (a,K)))
> 1
by sepsep;
H:
@ (
a,
K)
= a
by FIELD_7:def 4;
consider b being non
zero Element of
K,
q being
Ppoly of
K such that I:
p1 = b * q
by D, FIELD_4:def 5;
F:
p splits_in K
by I, FIELD_4:def 5;
E is
Subfield of
K
by FIELD_4:7;
then 0. K =
0. E
by EC_PF_1:def 1
.=
Ext_eval (
p,
a)
by B, mulzero, FIELD_4:def 2
.=
Ext_eval (
p,
(@ (a,K)))
by H, FIELD_6:11
;
hence
contradiction
by F, E, AS, ThSep0, FIELD_4:def 2;
verum end; hence
for
E being
FieldExtension of
F for
a being
Element of
E holds
multiplicity (
p,
a)
<= 1
;
verum end;
hence
( p is separable iff for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )
by A; verum