let F be Field; for p being non zero Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )
let p be non zero Element of the carrier of (Polynom-Ring F); for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )
let E be FieldExtension of F; ( p splits_in E implies ( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F ) )
assume AS:
p splits_in E
; ( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )
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) ;
p <> 0_. F
;
then
p1 <> 0_. E
by FIELD_4:12;
then reconsider p1 = p1 as non zero Element of the carrier of (Polynom-Ring E) by UPROOTS:def 5;
set g = p1 gcd ((Deriv E) . p1);
A:
now ( ex a being Element of E st multiplicity (p,a) > 1 implies p gcd ((Deriv F) . p) <> 1_. F )assume
ex
a being
Element of
E st
multiplicity (
p,
a)
> 1
;
p gcd ((Deriv F) . p) <> 1_. Fthen consider a being
Element of
E such that A1:
multiplicity (
p,
a)
> 1
;
A6:
multiplicity (
p1,
a)
= multiplicity (
p,
a)
by FIELD_14:def 6;
then A2:
a is_a_root_of p1
by A1, UPROOTS:52;
eval (
p1,
a)
= 0. E
by A6, A1, UPROOTS:52, POLYNOM5:def 7;
then A3:
rpoly (1,
a)
divides p1
by RING_5:11;
eval (
((Deriv E) . p1),
a)
= 0. E
by A1, A2, A6, multi4;
then
rpoly (1,
a)
divides (Deriv E) . p1
by RING_5:11;
then A4:
deg (rpoly (1,a)) <= deg (p1 gcd ((Deriv E) . p1))
by A3, RING_4:52, RING_5:13;
A5:
deg (rpoly (1,a)) = 1
by HURWITZ:27;
(
1_. E = (1. E) | E &
0. E <> 1. E )
by RING_4:14;
then A7:
p1 gcd ((Deriv E) . p1) <> 1_. E
by A4, A5, RING_4:21;
(
(Deriv E) . p1 = (Deriv F) . p &
1_. F = 1_. E )
by FIELD_14:66, FIELD_4:14;
hence
p gcd ((Deriv F) . p) <> 1_. F
by A7, FIELD_14:45;
verum end;
now ( p gcd ((Deriv F) . p) <> 1_. F implies ex a being Element of E st multiplicity (p,a) > 1 )assume B1:
p gcd ((Deriv F) . p) <> 1_. F
;
ex a being Element of E st multiplicity (p,a) > 1
(
(Deriv E) . p1 = (Deriv F) . p &
1_. F = 1_. E )
by FIELD_14:66, FIELD_4:14;
then
p1 gcd ((Deriv E) . p1) <> 1_. E
by B1, FIELD_14:45;
then B8:
(
p1 gcd ((Deriv E) . p1) divides p1 &
p1 gcd ((Deriv E) . p1) divides (Deriv E) . p1 &
deg (p1 gcd ((Deriv E) . p1)) > 0 )
by mm0, RING_4:52;
then reconsider g =
p1 gcd ((Deriv E) . p1) as non
constant Polynomial of
E by RATFUNC1:def 2;
consider r being
Polynomial of
E such that B2:
p1 = g *' r
by RING_4:52, RING_4:1;
consider b being non
zero Element of
E,
q being
Ppoly of
E such that M:
p = b * q
by AS, FIELD_4:def 5;
B10:
p1 splits_in E
by M, FIELD_4:def 5;
B9:
E is
FieldExtension of
E
by FIELD_4:6;
( not
r is
zero &
g is non
constant Polynomial of
E )
by B2;
then consider b being non
zero Element of
E,
q being
Ppoly of
E such that B5:
g = b * q
by B2, B10, B9, FIELD_13:7, FIELD_4:def 5;
consider a being
Element of
E such that B3:
a is_a_root_of q
by POLYNOM5:def 8;
eval (
(b * q),
a)
= b * (0. E)
by B3, RING_5:7;
then B7:
a is_a_root_of g
by B5;
then
a is_a_root_of p1
by mm1, RING_4:52;
then B9:
(
multiplicity (
p1,
a)
> 1 iff
eval (
((Deriv E) . p1),
a)
= 0. E )
by multi4;
multiplicity (
p1,
a)
= multiplicity (
p,
a)
by FIELD_14:def 6;
hence
ex
a being
Element of
E st
multiplicity (
p,
a)
> 1
by B7, B8, B9, POLYNOM5:def 7, mm1;
verum end;
hence
( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )
by A; verum