let F be non 2 -characteristic Field; for p being quadratic Element of the carrier of (Polynom-Ring F) holds
( F is SplittingField of p iff DC p is square )
let p be quadratic Element of the carrier of (Polynom-Ring F); ( F is SplittingField of p iff DC p is square )
consider a being non zero Element of F, b, c being Element of F such that
A:
p = <%c,b,a%>
by qua5;
B:
now ( DC p is square implies F is SplittingField of p )assume
DC p is
square
;
F is SplittingField of pthen
(b ^2) - ((4 '*' a) * c) is
square
by A, defDC;
then consider w being
Element of
F such that C:
w ^2 = (b ^2) - ((4 '*' a) * c)
by O_RING_1:def 2;
set r1 =
((- b) + w) * ((2 '*' a) ");
set r2 =
((- b) - w) * ((2 '*' a) ");
D:
<%c,b,a%> = a * ((X- (((- b) + w) * ((2 '*' a) "))) *' (X- (((- b) - w) * ((2 '*' a) "))))
by C, lemred;
(
rpoly (1,
(((- b) + w) * ((2 '*' a) "))) is
Ppoly of
F &
rpoly (1,
(((- b) - w) * ((2 '*' a) "))) is
Ppoly of
F )
by RING_5:51;
then E:
(rpoly (1,(((- b) + w) * ((2 '*' a) ")))) *' (rpoly (1,(((- b) - w) * ((2 '*' a) ")))) is
Ppoly of
F
by RING_5:52;
F:
F is
FieldExtension of
F
by FIELD_4:6;
hence
F is
SplittingField of
p
by E, F, A, D, FIELD_4:def 5, FIELD_8:def 1;
verum end;
hence
( F is SplittingField of p iff DC p is square )
by B; verum