:: Quadratic Extensions
:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: Received November 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

theorem lemmonus: :: FIELD_9:1

for a, b being Nat st a <= b holds
a -' 1 <= b -' 1

proof end;

registration

let i be Integer;

cluster i ^2 -> integer ;

coherence
i ^2 is integer

proof end;

end;

definition

let R be Ring;
let S be RingExtension of R;
let a be R -membered Element of S;

func @ a -> Element of R equals :: FIELD_9:def 1
a;

coherence
a is Element of R by FIELD_7:def 5;

end;

:: deftheorem defines @ FIELD_9:def 1 :
for R being Ring
for S being RingExtension of R
for a being b₁ -membered Element of S holds @ a = a;

registration

let R be Ring;
let S be RingExtension of R;
let a be R -membered Element of S;

cluster - a -> R -membered ;

coherence
- a is R -membered

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;
let a, b be R -membered Element of S;

cluster a + b -> R -membered ;

coherence
a + b is R -membered

proof end;

cluster a * b -> R -membered ;

coherence
a * b is R -membered

proof end;

end;

registration

let R be Ring;
let S be RingExtension of R;

cluster 0. S -> R -membered ;

coherence
0. S is R -membered

proof end;

end;

registration

let R be non degenerated Ring;
let S be RingExtension of R;

cluster 1. S -> non zero R -membered ;

coherence
( not 1. S is zero & 1. S is R -membered )

proof end;

end;

registration

let R be non degenerated Ring;
let S be RingExtension of R;

cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable R -membered for Element of the carrier of S;

existence
ex b₁ being Element of S st
( not b₁ is zero & b₁ is R -membered )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a be non zero F -membered Element of E;

cluster / a -> F -membered ;

coherence
a " is F -membered

proof end;

end;

registration

let R be Ring;
let a, b, c be Element of R;

cluster <*a,b,c*> -> the carrier of R -valued ;

coherence
<*a,b,c*> is the carrier of R -valued

proof end;

end;

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible strict right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( INT.Ring ) V324() non 2 -characteristic for doubleLoopStr ;

existence
ex b₁ being Field st
( not b₁ is 2 -characteristic & b₁ is strict )

proof end;

end;

registration

let R be Ring;

reduce (0. R) ^2 to 0. R;

reducibility
(0. R) ^2 = 0. R

proof end;

reduce (1. R) ^2 to 1. R;

reducibility
(1. R) ^2 = 1. R

proof end;

reduce (- (1. R)) ^2 to 1. R;

reducibility
(- (1. R)) ^2 = 1. R

proof end;

end;

theorem ch0: :: FIELD_9:2

for R being comRing
for a, b being Element of R holds (a * b) ^2 = (a ^2) * (b ^2)

proof end;

theorem ch0a: :: FIELD_9:3

for F being Field
for a being Element of F
for b being non zero Element of F
for i being Integer st i '*' a <> 0. F & i '*' b <> 0. F holds
(i '*' a) * ((i '*' b) ") = a * (b ")

proof end;

theorem ch1: :: FIELD_9:4

for R being comRing
for a being Element of R
for i being Integer holds (i '*' a) ^2 = (i ^2) '*' (a ^2)

proof end;

theorem ch2: :: FIELD_9:5

for R being non 2 -characteristic domRing
for a being Element of R holds
( 2 '*' a = 0. R iff a = 0. R )

proof end;

theorem ch4: :: FIELD_9:6

for R being non 2 -characteristic domRing
for a being Element of R holds
( 4 '*' a = 0. R iff a = 0. R )

proof end;

theorem Z3: :: FIELD_9:7

for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st b = a holds
for i being Integer holds i '*' a = i '*' b

proof end;

theorem lemquadr: :: FIELD_9:8

for R being domRing
for S being domRingExtension of R
for a being Element of R
for b being Element of S holds
( not b ^2 = a ^2 or b = a or b = - a )

proof end;

theorem ext1: :: FIELD_9:9

for F being Field
for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})

proof end;

theorem :: FIELD_9:10

for F being Field
for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a}) = FAdj (F,{(- a)})

proof end;

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( INT.Ring ) V324() non algebraic-closed polynomial_disjoint for doubleLoopStr ;

existence
not for b₁ being polynomial_disjoint Field holds b₁ is algebraic-closed

proof end;

end;

registration

let F be non algebraic-closed Field;

cluster Relation-like NAT -defined the carrier of F -valued Function-like non empty V14( NAT ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support irreducible non linear for Element of the carrier of (Polynom-Ring F);

existence
ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is irreducible & not b₁ is linear )

proof end;

end;

registration

let F be Field;

cluster irreducible non linear -> non with_roots for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st b₁ is irreducible & not b₁ is linear holds
not b₁ is with_roots ;

cluster irreducible with_roots -> linear for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st b₁ is irreducible & b₁ is with_roots holds
b₁ is linear ;

end;

registration

let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);

cluster KrRootP p -> F -algebraic ;

coherence
KrRootP p is F -algebraic

proof end;

end;

registration

let F be non algebraic-closed polynomial_disjoint Field;
let p be irreducible non linear Element of the carrier of (Polynom-Ring F);

cluster KrRootP p -> non zero non F -membered ;

coherence
( not KrRootP p is zero & not KrRootP p is F -membered )

proof end;

end;

leng: for R being Ring
for p, q being Polynomial of R holds len (p *' q) <= ((len p) + (len q)) -' 1

proof end;

theorem :: FIELD_9:11

for R being non degenerated Ring
for p being non zero Polynomial of R
for q being Polynomial of R holds deg (p *' q) <= (deg p) + (deg q)

proof end;

registration

let L be non degenerated well-unital doubleLoopStr ;
let k be non zero Element of NAT ;
let a be Element of L;

cluster rpoly (k,a) -> monic ;

coherence
rpoly (k,a) is monic

proof end;

end;

registration

let R be non degenerated Ring;
let a be non zero Element of R;
let b be Element of R;

cluster <%b,a%> -> linear ;

coherence
<%b,a%> is linear

proof end;

end;

registration

let R be non degenerated Ring;
let b be Element of R;

cluster <%b,(1. R)%> -> monic linear ;

coherence
( <%b,(1. R)%> is monic & <%b,(1. R)%> is linear )

proof end;

end;

theorem qua20: :: FIELD_9:12

for R being Ring
for a, b, x being Element of R holds x * <%b,a%> = <%(x * b),(x * a)%>

proof end;

theorem deg2: :: FIELD_9:13

for R being Ring
for p being Polynomial of R st deg p < 2 holds
for a being Element of R ex y, z being Element of R st p = <%y,z%>

proof end;

theorem :: FIELD_9:14

for R being comRing
for p being Polynomial of R st deg p < 2 holds
for a being Element of R ex y, z being Element of R st eval (p,a) = y + (a * z)

proof end;

theorem deg2evale: :: FIELD_9:15

for F being Field
for E being FieldExtension of F
for p being Polynomial of F st deg p < 2 holds
for a being Element of E ex y, z being b₁ -membered Element of E st Ext_eval (p,a) = y + (a * z)

proof end;

definition

let R be Ring;
let a be Element of R;

func X- a -> Element of the carrier of (Polynom-Ring R) equals :: FIELD_9:def 2
rpoly (1,a);

coherence
rpoly (1,a) is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

func X+ a -> Element of the carrier of (Polynom-Ring R) equals :: FIELD_9:def 3
rpoly (1,(- a));

coherence
rpoly (1,(- a)) is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

end;

:: deftheorem defines X- FIELD_9:def 2 :
for R being Ring
for a being Element of R holds X- a = rpoly (1,a);

:: deftheorem defines X+ FIELD_9:def 3 :
for R being Ring
for a being Element of R holds X+ a = rpoly (1,(- a));

registration

let R be non degenerated Ring;
let a be Element of R;

cluster X- a -> monic linear ;

coherence
( X- a is linear & X- a is monic )

proof end;

cluster X+ a -> monic linear ;

coherence
( X+ a is linear & X+ a is monic )

proof end;

end;

definition

let R be Ring;
let p be Polynomial of R;

attr p is quadratic means :defquadr: :: FIELD_9:def 4
deg p = 2;

end;

:: deftheorem defquadr defines quadratic FIELD_9:def 4 :
for R being Ring
for p being Polynomial of R holds
( p is quadratic iff deg p = 2 );

registration

let R be non degenerated Ring;

cluster Relation-like NAT -defined the carrier of R -valued Function-like non empty V14( NAT ) quasi_total finite-Support monic quadratic for Element of bool [:NAT, the carrier of R:];

existence
ex b₁ being Polynomial of R st
( b₁ is monic & b₁ is quadratic )

proof end;

cluster Relation-like NAT -defined the carrier of R -valued Function-like non empty V14( NAT ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support monic quadratic for Element of the carrier of (Polynom-Ring R);

existence
ex b₁ being Element of the carrier of (Polynom-Ring R) st
( b₁ is monic & b₁ is quadratic )

proof end;

end;

registration

let R be non degenerated Ring;

cluster Function-like quasi_total finite-Support quadratic -> non constant quadratic for Element of bool [:NAT, the carrier of R:];

coherence
for b₁ being quadratic Polynomial of R holds not b₁ is constant

proof end;

cluster quadratic -> non constant quadratic for Element of the carrier of (Polynom-Ring R);

coherence
for b₁ being quadratic Element of the carrier of (Polynom-Ring R) holds not b₁ is constant

proof end;

end;

definition

let L be non empty ZeroStr ;
let a, b, c be Element of L;

func <%c,b,a%> -> sequence of L equals :: FIELD_9:def 5
(((0_. L) +* (0,c)) +* (1,b)) +* (2,a);

correctness
coherence
(((0_. L) +* (0,c)) +* (1,b)) +* (2,a) is sequence of L;
;

end;

:: deftheorem defines <% FIELD_9:def 5 :
for L being non empty ZeroStr
for a, b, c being Element of L holds <%c,b,a%> = (((0_. L) +* (0,c)) +* (1,b)) +* (2,a);

qua1: for L being non empty ZeroStr
for a, b, c being Element of L holds
( <%c,b,a%> . 0 = c & <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) )

proof end;

registration

let L be non empty ZeroStr ;
let a, b, c be Element of L;

cluster <%c,b,a%> -> finite-Support ;

coherence
<%c,b,a%> is finite-Support

proof end;

end;

theorem :: FIELD_9:16

for L being non empty ZeroStr
for a, b, c being Element of L holds
( <%c,b,a%> . 0 = c & <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) ) by qua1;

qua2: for L being non empty ZeroStr
for a, b, c being Element of L holds len <%c,b,a%> <= 3

proof end;

theorem :: FIELD_9:17

for L being non empty ZeroStr
for a, b, c being Element of L holds deg <%c,b,a%> <= 2

proof end;

qua3: for L being non empty ZeroStr
for a, b, c being Element of L st a <> 0. L holds
len <%c,b,a%> = 3

proof end;

theorem qua4: :: FIELD_9:18

for L being non empty ZeroStr
for a, b, c being Element of L holds
( deg <%c,b,a%> = 2 iff a <> 0. L )

proof end;

registration

let R be non degenerated Ring;
let a be non zero Element of R;
let b, c be Element of R;

cluster <%c,b,a%> -> quadratic ;

coherence
<%c,b,a%> is quadratic by qua4;

end;

registration

let R be non degenerated Ring;
let b, c be Element of R;

cluster <%c,b,(1. R)%> -> monic quadratic ;

coherence
( <%c,b,(1. R)%> is quadratic & <%c,b,(1. R)%> is monic )

proof end;

end;

registration

let R be domRing;
let a, x be non zero Element of R;
let b, c be Element of R;

cluster x * <%c,b,a%> -> quadratic ;

coherence
x * <%c,b,a%> is quadratic

proof end;

end;

theorem qua6: :: FIELD_9:19

for R being Ring
for a, b, c, x being Element of R holds x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%>

proof end;

theorem evalq: :: FIELD_9:20

for R being Ring
for a, b, c, x being Element of R holds eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))

proof end;

theorem qua5: :: FIELD_9:21

for R being non degenerated Ring
for p being Polynomial of R holds
( p is quadratic iff ex a being non zero Element of R ex b, c being Element of R st p = <%c,b,a%> )

proof end;

theorem qua5a: :: FIELD_9:22

for R being non degenerated Ring
for p being monic Polynomial of R holds
( p is quadratic iff ex b, c being Element of R st p = <%c,b,(1. R)%> )

proof end;

theorem eval2: :: FIELD_9:23

for R being non degenerated Ring
for S being RingExtension of R
for a1, b1, c1 being Element of R
for a2, b2, c2 being Element of S st a1 = a2 & b1 = b2 & c1 = c2 holds
<%c2,b2,a2%> = <%c1,b1,a1%>

proof end;

definition

let R be non degenerated Ring;
let p be Polynomial of R;

attr p is purely_quadratic means :defpur: :: FIELD_9:def 6
ex a being non zero Element of R ex c being Element of R st p = <%c,(0. R),a%>;

end;

:: deftheorem defpur defines purely_quadratic FIELD_9:def 6 :
for R being non degenerated Ring
for p being Polynomial of R holds
( p is purely_quadratic iff ex a being non zero Element of R ex c being Element of R st p = <%c,(0. R),a%> );

registration

let R be non degenerated Ring;
let a be non zero Element of R;
let c be Element of R;

cluster <%c,(0. R),a%> -> purely_quadratic ;

coherence
<%c,(0. R),a%> is purely_quadratic ;

end;

registration

let R be non degenerated Ring;

cluster Relation-like NAT -defined the carrier of R -valued Function-like non empty V14( NAT ) quasi_total finite-Support monic purely_quadratic for Element of bool [:NAT, the carrier of R:];

existence
ex b₁ being Polynomial of R st
( b₁ is monic & b₁ is purely_quadratic )

proof end;

end;

registration

let R be non degenerated Ring;

cluster Function-like quasi_total finite-Support purely_quadratic -> quadratic for Element of bool [:NAT, the carrier of R:];

coherence
for b₁ being Polynomial of R st b₁ is purely_quadratic holds
b₁ is quadratic ;

end;

definition

let R be Ring;
let a be Element of R;

func X^2- a -> Element of the carrier of (Polynom-Ring R) equals :: FIELD_9:def 7
<%(- a),(0. R),(1. R)%>;

coherence
<%(- a),(0. R),(1. R)%> is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

func X^2+ a -> Element of the carrier of (Polynom-Ring R) equals :: FIELD_9:def 8
<%a,(0. R),(1. R)%>;

coherence
<%a,(0. R),(1. R)%> is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

end;

:: deftheorem defines X^2- FIELD_9:def 7 :
for R being Ring
for a being Element of R holds X^2- a = <%(- a),(0. R),(1. R)%>;

:: deftheorem defines X^2+ FIELD_9:def 8 :
for R being Ring
for a being Element of R holds X^2+ a = <%a,(0. R),(1. R)%>;

registration

let R be non degenerated Ring;

cluster Function-like quasi_total finite-Support linear -> non quadratic for Element of bool [:NAT, the carrier of R:];

coherence
for b₁ being Polynomial of R st b₁ is linear holds
not b₁ is quadratic by FIELD_5:def 1;

cluster Function-like quasi_total finite-Support quadratic -> non linear for Element of bool [:NAT, the carrier of R:];

coherence
for b₁ being Polynomial of R st b₁ is quadratic holds
not b₁ is linear ;

end;

registration

let R be non degenerated Ring;
let a be Element of R;

cluster X^2- a -> monic non constant purely_quadratic ;

coherence
( X^2- a is purely_quadratic & X^2- a is monic & not X^2- a is constant ) ;

cluster X^2+ a -> monic non constant purely_quadratic ;

coherence
( X^2+ a is purely_quadratic & X^2+ a is monic & not X^2+ a is constant ) ;

end;

theorem lemred1: :: FIELD_9:24

for F being Field
for b1, c1, b2, c2 being Element of F holds <%c1,b1%> *' <%c2,b2%> = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%>

proof end;

lemred3: for F being Field
for c1, c2 being Element of F holds <%(- c1),(1. F)%> *' <%(- c2),(1. F)%> = <%(c1 * c2),(- (c1 + c2)),(1. F)%>

proof end;

lemred3z: for F being Field
for c1, c2 being Element of F holds (rpoly (1,c1)) *' (rpoly (1,c2)) = <%(c1 * c2),(- (c1 + c2)),(1. F)%>

proof end;

theorem lemeval: :: FIELD_9:25

for F being non 2 -characteristic Field
for a being non zero Element of F
for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
( eval (<%c,b,a%>,(((- b) + w) * ((2 '*' a) "))) = 0. F & eval (<%c,b,a%>,(((- b) - w) * ((2 '*' a) "))) = 0. F )

proof end;

theorem lemeval2: :: FIELD_9:26

for F being Field
for a being non zero Element of F
for b, c being Element of F st Roots <%c,b,a%> <> {} holds
(b ^2) - ((4 '*' a) * c) is square

proof end;

theorem TC0: :: FIELD_9:27

for F being non 2 -characteristic Field
for a being non zero Element of F
for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}

proof end;

theorem lemred: :: FIELD_9:28

for F being non 2 -characteristic Field
for a being non zero Element of F
for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))

proof end;

definition

let R be non degenerated Ring;
let p be quadratic Polynomial of R;

func Discriminant p -> Element of R means :defDC: :: FIELD_9:def 9
ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & it = (b ^2) - ((4 '*' a) * c) );

existence
ex b₁ being Element of R ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₁ = (b ^2) - ((4 '*' a) * c) )

proof end;

uniqueness
for b₁, b₂ being Element of R st ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₁ = (b ^2) - ((4 '*' a) * c) ) & ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₂ = (b ^2) - ((4 '*' a) * c) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defDC defines Discriminant FIELD_9:def 9 :
for R being non degenerated Ring
for p being quadratic Polynomial of R
for b₃ being Element of R holds
( b₃ = Discriminant p iff ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₃ = (b ^2) - ((4 '*' a) * c) ) );

notation

let R be non degenerated Ring;
let p be quadratic Polynomial of R;
synonym DC p for Discriminant p;

end;

definition

let R be non degenerated Ring;
let p be monic quadratic Polynomial of R;

redefine func Discriminant p means :defDCm: :: FIELD_9:def 10
ex b, c being Element of R st
( p = <%c,b,(1. R)%> & it = (b ^2) - (4 '*' c) );

compatibility
for b₁ being Element of R holds
( b₁ = Discriminant p iff ex b, c being Element of R st
( p = <%c,b,(1. R)%> & b₁ = (b ^2) - (4 '*' c) ) )

proof end;

end;

:: deftheorem defDCm defines Discriminant FIELD_9:def 10 :
for R being non degenerated Ring
for p being monic quadratic Polynomial of R
for b₃ being Element of R holds
( b₃ = Discriminant p iff ex b, c being Element of R st
( p = <%c,b,(1. R)%> & b₃ = (b ^2) - (4 '*' c) ) );

definition

let R be non degenerated Ring;
let p be monic purely_quadratic Polynomial of R;

redefine func Discriminant p means :defDCpq: :: FIELD_9:def 11
ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & it = - (4 '*' c) );

compatibility
for b₁ being Element of R holds
( b₁ = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b₁ = - (4 '*' c) ) )

proof end;

end;

:: deftheorem defDCpq defines Discriminant FIELD_9:def 11 :
for R being non degenerated Ring
for p being monic purely_quadratic Polynomial of R
for b₃ being Element of R holds
( b₃ = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b₃ = - (4 '*' c) ) );

theorem TC1: :: FIELD_9:29

for F being non 2 -characteristic Field
for p being quadratic Polynomial of F holds
( Roots p <> {} iff DC p is square )

proof end;

theorem :: FIELD_9:30

for F being non 2 -characteristic Field
for p being quadratic Polynomial of F holds
( card (Roots p) = 1 iff DC p = 0. F )

proof end;

theorem :: FIELD_9:31

for F being non 2 -characteristic Field
for p being quadratic Polynomial of F holds
( card (Roots p) = 2 iff ( not DC p is zero & DC p is square ) )

proof end;

theorem naH: :: FIELD_9:32

for F being non 2 -characteristic Field
for p being quadratic Element of the carrier of (Polynom-Ring F) holds
( p is reducible iff DC p is square )

proof end;

theorem naH2: :: FIELD_9:33

for F being non 2 -characteristic Field
for a being Element of F holds
( X^2- a is reducible iff a is square )

proof end;

theorem cz2: :: FIELD_9:34

the carrier of (Z/ 2) = {(0. (Z/ 2)),(1. (Z/ 2))}

proof end;

theorem cz2a: :: FIELD_9:35

- (1. (Z/ 2)) = 1. (Z/ 2) by FIELD_3:4, RLVECT_1:def 10;

registration

cluster INT.Ring 2 -> polynomial_disjoint ;

coherence
Z/ 2 is polynomial_disjoint

proof end;

end;

registration

cluster -> square for Element of the carrier of (Z/ 2);

coherence
for b₁ being Element of (Z/ 2) holds b₁ is square

proof end;

end;

registration

cluster Function-like quasi_total finite-Support non zero -> non zero monic for Element of bool [:NAT, the carrier of (Z/ 2):];

coherence
for b₁ being non zero Polynomial of (Z/ 2) holds b₁ is monic

proof end;

cluster non zero -> non zero monic for Element of the carrier of (Polynom-Ring (Z/ 2));

coherence
for b₁ being non zero Element of the carrier of (Polynom-Ring (Z/ 2)) holds b₁ is monic ;

end;

definition

func X^2 -> quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 12
<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> is quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

func X^2+1 -> quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 13
<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%> is quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

func X^2+X -> quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 14
<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> is quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

func X^2+X+1 -> quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 15
<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> is quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

func X_ -> linear Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 16
<%(0. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(0. (Z/ 2)),(1. (Z/ 2))%> is linear Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

func X-1 -> linear Element of the carrier of (Polynom-Ring (Z/ 2)) equals :: FIELD_9:def 17
<%(1. (Z/ 2)),(1. (Z/ 2))%>;

coherence
<%(1. (Z/ 2)),(1. (Z/ 2))%> is linear Element of the carrier of (Polynom-Ring (Z/ 2)) by POLYNOM3:def 10;

end;

:: deftheorem defines X^2 FIELD_9:def 12 :
X^2 = <%(0. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>;

:: deftheorem defines X^2+1 FIELD_9:def 13 :
X^2+1 = <%(1. (Z/ 2)),(0. (Z/ 2)),(1. (Z/ 2))%>;

:: deftheorem defines X^2+X FIELD_9:def 14 :
X^2+X = <%(0. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;

:: deftheorem defines X^2+X+1 FIELD_9:def 15 :
X^2+X+1 = <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%>;

:: deftheorem defines X_ FIELD_9:def 16 :
X_ = <%(0. (Z/ 2)),(1. (Z/ 2))%>;

:: deftheorem defines X-1 FIELD_9:def 17 :
X-1 = <%(1. (Z/ 2)),(1. (Z/ 2))%>;

theorem pz2: :: FIELD_9:36

{ p where p is quadratic Polynomial of (Z/ 2) : verum } = {X^2,X^2+1,X^2+X,X^2+X+1}

proof end;

theorem :: FIELD_9:37

card { p where p is quadratic Polynomial of (Z/ 2) : verum } = 4

proof end;

theorem :: FIELD_9:38

for p being quadratic Polynomial of (Z/ 2) holds DC p is square ;

theorem z21: :: FIELD_9:39

( X^2 = X_ *' X_ & Roots X^2 = {(0. (Z/ 2))} )

proof end;

theorem z22: :: FIELD_9:40

( X^2+1 = X-1 *' X-1 & Roots X^2+1 = {(1. (Z/ 2))} )

proof end;

theorem z23: :: FIELD_9:41

( X^2+X = X_ *' X-1 & Roots X^2+X = {(0. (Z/ 2)),(1. (Z/ 2))} )

proof end;

theorem z24: :: FIELD_9:42

Roots X^2+X+1 = {}

proof end;

registration

cluster X^2 -> reducible quadratic ;

coherence
not X^2 is irreducible by z21;

cluster X^2+1 -> reducible quadratic ;

coherence
not X^2+1 is irreducible by z22;

cluster X^2+X -> reducible quadratic ;

coherence
not X^2+X is irreducible by z23;

cluster X^2+X+1 -> irreducible quadratic ;

coherence
X^2+X+1 is irreducible

proof end;

end;

z25: for p being quadratic Polynomial of (Z/ 2) holds
( p splits_in Z/ 2 iff p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> )

proof end;

z26: for p being quadratic Element of the carrier of (Polynom-Ring (Z/ 2)) st p <> <%(1. (Z/ 2)),(1. (Z/ 2)),(1. (Z/ 2))%> holds
Z/ 2 is SplittingField of p

proof end;

theorem :: FIELD_9:43

Z/ 2 is SplittingField of X^2

proof end;

theorem :: FIELD_9:44

Z/ 2 is SplittingField of X^2+1

proof end;

theorem :: FIELD_9:45

Z/ 2 is SplittingField of X^2+X

proof end;

definition

func alpha -> Element of (embField (canHomP X^2+X+1)) equals :: FIELD_9:def 18
KrRootP X^2+X+1;

coherence
KrRootP X^2+X+1 is Element of (embField (canHomP X^2+X+1)) ;

end;

:: deftheorem defines alpha FIELD_9:def 18 :
alpha = KrRootP X^2+X+1;

definition

func alpha-1 -> Element of (embField (canHomP X^2+X+1)) equals :: FIELD_9:def 19
alpha - (1. (embField (canHomP X^2+X+1)));

coherence
alpha - (1. (embField (canHomP X^2+X+1))) is Element of (embField (canHomP X^2+X+1)) ;

end;

:: deftheorem defines alpha-1 FIELD_9:def 19 :
alpha-1 = alpha - (1. (embField (canHomP X^2+X+1)));

registration

cluster alpha -> non zero Z/ 2 -algebraic ;

coherence
( not alpha is zero & alpha is Z/ 2 -algebraic ) ;

end;

lemZ2: ( X^2+X+1 = (X- alpha) *' (X- (alpha ")) & alpha " = - (alpha + (1. (embField (canHomP X^2+X+1)))) & - alpha = (alpha ") + (1. (embField (canHomP X^2+X+1))) )

proof end;

theorem lemalph: :: FIELD_9:46

( - alpha = alpha & alpha " = alpha-1 & alpha " <> alpha )

proof end;

theorem :: FIELD_9:47

( X^2+X+1 = (X- alpha) *' (X- (alpha ")) & (X- alpha) *' (X- (alpha ")) = (X- alpha) *' (X- alpha-1) ) by lemZ2, lemalph;

theorem lemZ2roots: :: FIELD_9:48

Roots ((FAdj ((Z/ 2),{alpha})),X^2+X+1) = {alpha,alpha-1}

proof end;

theorem :: FIELD_9:49

card (Roots ((FAdj ((Z/ 2),{alpha})),X^2+X+1)) = 2 by lemZ2roots, lemalph, CARD_2:57;

theorem lemZ2min: :: FIELD_9:50

MinPoly (alpha,(Z/ 2)) = X^2+X+1

proof end;

theorem :: FIELD_9:51

deg ((FAdj ((Z/ 2),{alpha})),(Z/ 2)) = 2

proof end;

theorem :: FIELD_9:52

FAdj ((Z/ 2),{alpha}) is SplittingField of X^2+X+1

proof end;

definition

let R be Ring;

attr R is quadratic_complete means :defqc: :: FIELD_9:def 20
the carrier of R c= SQ R;

end;

:: deftheorem defqc defines quadratic_complete FIELD_9:def 20 :
for R being Ring holds
( R is quadratic_complete iff the carrier of R c= SQ R );

registration

cluster - (1. F_Real) -> non square ;

coherence
not - (1. F_Real) is being_a_square

proof end;

cluster - (1. F_Rat) -> non square ;

coherence
not - (1. F_Rat) is being_a_square

proof end;

end;

registration

cluster non empty non degenerated right_complementable well-unital V116() V127() V128() V129() V139() algebraic-closed -> non degenerated quadratic_complete for doubleLoopStr ;

coherence
for b₁ being non degenerated Ring st b₁ is algebraic-closed holds
b₁ is quadratic_complete

proof end;

cluster non empty non degenerated right_complementable well-unital V116() V127() V128() V129() V139() preordered -> non degenerated non quadratic_complete for doubleLoopStr ;

coherence
for b₁ being non degenerated Ring st b₁ is preordered holds
not b₁ is quadratic_complete

proof end;

end;

registration

cluster F_Rat -> non quadratic_complete ;

coherence
not F_Rat is quadratic_complete ;

cluster F_Real -> non quadratic_complete ;

coherence
not F_Real is quadratic_complete ;

cluster F_Complex -> quadratic_complete ;

coherence
F_Complex is quadratic_complete ;

end;

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible strict right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( INT.Ring ) V324() polynomial_disjoint non quadratic_complete for doubleLoopStr ;

existence
ex b₁ being Field st
( not b₁ is quadratic_complete & b₁ is polynomial_disjoint & b₁ is strict )

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible strict right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( INT.Ring ) V324() quadratic_complete for doubleLoopStr ;

existence
ex b₁ being Field st
( b₁ is quadratic_complete & b₁ is strict )

proof end;

end;

registration

cluster non empty right_complementable well-unital V116() V127() V128() V129() V139() non quadratic_complete -> non degenerated for doubleLoopStr ;

coherence
for b₁ being Ring st not b₁ is quadratic_complete holds
not b₁ is degenerated

proof end;

end;

registration

let R be non quadratic_complete Ring;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non square for Element of the carrier of R;

existence
not for b₁ being Element of R holds b₁ is square

proof end;

end;

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible strict right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( INT.Ring ) V324() non 2 -characteristic polynomial_disjoint non quadratic_complete for doubleLoopStr ;

existence
ex b₁ being Field st
( b₁ is strict & b₁ is polynomial_disjoint & not b₁ is quadratic_complete & not b₁ is 2 -characteristic )

proof end;

end;

registration

let F be non 2 -characteristic non quadratic_complete Field;

cluster Relation-like NAT -defined the carrier of F -valued Function-like non empty V14( NAT ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support monic irreducible quadratic for Element of the carrier of (Polynom-Ring F);

existence
ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is monic & b₁ is quadratic & b₁ is irreducible )

proof end;

end;

registration

let F be non 2 -characteristic Field;
let a be square Element of F;

cluster X^2- a -> reducible ;

coherence
not X^2- a is irreducible by naH2;

end;

registration

let F be non 2 -characteristic non quadratic_complete Field;
let a be non square Element of F;

cluster X^2- a -> irreducible ;

coherence
X^2- a is irreducible by naH2;

end;

definition

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let a be non square Element of F;

func sqrt a -> Element of (embField (canHomP (X^2- a))) equals :: FIELD_9:def 21
KrRootP (X^2- a);

coherence
KrRootP (X^2- a) is Element of (embField (canHomP (X^2- a))) ;

end;

:: deftheorem defines sqrt FIELD_9:def 21 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds sqrt a = KrRootP (X^2- a);

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let a be non square Element of F;

cluster sqrt a -> non zero F -algebraic ;

coherence
( not sqrt a is zero & sqrt a is F -algebraic )

proof end;

end;

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let a be non square Element of F;

cluster embField (canHomP (X^2- a)) -> FAdj (F,{(sqrt a)}) -extending ;

coherence
embField (canHomP (X^2- a)) is FAdj (F,{(sqrt a)}) -extending by FIELD_4:7;

end;

m30: for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds MinPoly ((sqrt a),F) = X^2- a

proof end;

dega: for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds deg ((FAdj (F,{(sqrt a)})),F) = 2

proof end;

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let a be non square Element of F;

cluster sqrt a -> non F -membered FAdj (F,{(sqrt a)}) -membered ;

coherence
( sqrt a is FAdj (F,{(sqrt a)}) -membered & not sqrt a is F -membered )

proof end;

end;

theorem m1: :: FIELD_9:53

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds (sqrt a) * (sqrt a) = a

proof end;

theorem :: FIELD_9:54

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds MinPoly ((sqrt a),F) = X^2- a by m30;

theorem :: FIELD_9:55

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds deg ((FAdj (F,{(sqrt a)})),F) = 2 by dega;

theorem Fi1a: :: FIELD_9:56

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds (X- (sqrt a)) *' (X+ (sqrt a)) = X^2- a

proof end;

theorem Fi2a: :: FIELD_9:57

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds Roots ((FAdj (F,{(sqrt a)})),(X^2- a)) = {(sqrt a),(- (sqrt a))}

proof end;

theorem Fi3a: :: FIELD_9:58

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds FAdj (F,{(sqrt a)}) is SplittingField of X^2- a

proof end;

qbase1: for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds Base (sqrt a) = {(1. F),(sqrt a)}

proof end;

theorem qbase4: :: FIELD_9:59

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds {(1. F),(sqrt a)} is Basis of (VecSp ((FAdj (F,{(sqrt a)})),F))

proof end;

qbase2: for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F
for x being object holds
( x in the carrier of (FAdj (F,{(sqrt a)})) iff ex y, z being b₁ -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) )

proof end;

theorem :: FIELD_9:60

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds the carrier of (FAdj (F,{(sqrt a)})) = { (y + ((@ (sqrt a)) * z)) where y, z is b₁ -membered Element of (FAdj (F,{(sqrt a)})) : verum }

proof end;

theorem :: FIELD_9:61

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F
for a1, a2, b1, b2 being b₁ -membered Element of (FAdj (F,{(sqrt a)})) st a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) holds
( a1 = a2 & b1 = b2 )

proof end;

definition

let F be non 2 -characteristic Field;
let p be quadratic Element of the carrier of (Polynom-Ring F);

attr p is DC-square means :defDCps: :: FIELD_9:def 22
DC p is square ;

end;

:: deftheorem defDCps defines DC-square FIELD_9:def 22 :
for F being non 2 -characteristic Field
for p being quadratic Element of the carrier of (Polynom-Ring F) holds
( p is DC-square iff DC p is square );

registration

let F be non 2 -characteristic Field;

cluster Relation-like NAT -defined the carrier of F -valued Function-like non empty V14( NAT ) quasi_total non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero monic non unital V322( Polynom-Ring F) V323( Polynom-Ring F) non constant quadratic DC-square for Element of the carrier of (Polynom-Ring F);

existence
ex b₁ being quadratic Element of the carrier of (Polynom-Ring F) st
( b₁ is monic & b₁ is DC-square )

proof end;

end;

registration

let F be non 2 -characteristic non quadratic_complete Field;

cluster Relation-like NAT -defined the carrier of F -valued Function-like non empty V14( NAT ) quasi_total non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero monic non unital V322( Polynom-Ring F) V323( Polynom-Ring F) non constant quadratic non DC-square for Element of the carrier of (Polynom-Ring F);

existence
ex b₁ being quadratic Element of the carrier of (Polynom-Ring F) st
( b₁ is monic & not b₁ is DC-square )

proof end;

end;

registration

let F be non 2 -characteristic non quadratic_complete Field;
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F);

cluster Discriminant p -> non square ;

coherence
not DC p is being_a_square by defDCps;

end;

registration

let F be non 2 -characteristic non quadratic_complete Field;
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F);

cluster X^2- (DC p) -> irreducible ;

coherence
X^2- (DC p) is irreducible ;

end;

registration

let F be non 2 -characteristic Field;
let p be quadratic DC-square Element of the carrier of (Polynom-Ring F);

cluster X^2- (DC p) -> reducible ;

coherence
not X^2- (DC p) is irreducible

proof end;

end;

theorem :: FIELD_9:62

for F being 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 )

proof end;

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F);

cluster sqrt (DC p) -> non zero F -algebraic ;

coherence
( not sqrt (DC p) is zero & sqrt (DC p) is F -algebraic ) ;

end;

definition

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F);

func RootDC p -> Element of (FAdj (F,{(sqrt (DC p))})) equals :: FIELD_9:def 23
sqrt (DC p);

coherence
sqrt (DC p) is Element of (FAdj (F,{(sqrt (DC p))}))

proof end;

end;

:: deftheorem defines RootDC FIELD_9:def 23 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds RootDC p = sqrt (DC p);

definition

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F);

func Root1 p -> Element of (FAdj (F,{(sqrt (DC p))})) equals :: FIELD_9:def 24
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");

coherence
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ") is Element of (FAdj (F,{(sqrt (DC p))})) ;

func Root2 p -> Element of (FAdj (F,{(sqrt (DC p))})) equals :: FIELD_9:def 25
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");

coherence
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ") is Element of (FAdj (F,{(sqrt (DC p))})) ;

end;

:: deftheorem defines Root1 FIELD_9:def 24 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Root1 p = ((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");

:: deftheorem defines Root2 FIELD_9:def 25 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Root2 p = ((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");

theorem Z1: :: FIELD_9:63

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds (RootDC p) * (RootDC p) = DC p

proof end;

theorem Z2: :: FIELD_9:64

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F)
for a being non zero Element of (FAdj (F,{(sqrt (DC p))}))
for b, c being Element of (FAdj (F,{(sqrt (DC p))})) st p = <%c,b,a%> holds
( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )

proof end;

theorem Z5: :: FIELD_9:65

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))

proof end;

theorem Z4: :: FIELD_9:66

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Roots ((FAdj (F,{(sqrt (DC p))})),p) = {(Root1 p),(Root2 p)}

proof end;

theorem :: FIELD_9:67

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Root1 p <> Root2 p

proof end;

theorem :: FIELD_9:68

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds deg ((FAdj (F,{(sqrt (DC p))})),F) = 2 by dega;

theorem :: FIELD_9:69

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds FAdj (F,{(sqrt (DC p))}) is SplittingField of p

proof end;

definition

let F be Field;
let E be FieldExtension of F;

attr E is F -quadratic means :: FIELD_9:def 26
deg (E,F) = 2;

end;

:: deftheorem defines -quadratic FIELD_9:def 26 :
for F being Field
for E being FieldExtension of F holds
( E is F -quadratic iff deg (E,F) = 2 );

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital V116() left_unital V127() V128() V129() V134() unital V139() V141() domRing-like V216() V217() V218() V219() V299() V319( Polynom-Ring F) V324() F -extending F -quadratic for doubleLoopStr ;

existence
ex b₁ being FieldExtension of F st b₁ is F -quadratic

proof end;

end;

registration

let F be Field;

cluster non empty non degenerated right_complementable almost_left_invertible well-unital V116() V127() V128() V129() V139() V141() F -extending F -quadratic -> F -finite for doubleLoopStr ;

coherence
for b₁ being FieldExtension of F st b₁ is F -quadratic holds
b₁ is F -finite

proof end;

end;

registration

let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field;
let a be non square Element of F;

cluster FieldAdjunction (F,{(sqrt a)}) -> F -quadratic ;

coherence
FAdj (F,{(sqrt a)}) is F -quadratic by dega;

end;

theorem m105: :: FIELD_9:70

for F being Field
for a, b being Element of F st b ^2 = a holds
eval ((X^2- a),b) = 0. F

proof end;

theorem m102: :: FIELD_9:71

for F being non 2 -characteristic Field
for E being FieldExtension of F
for a being Element of F st ( for b being Element of F holds not a = b ^2 ) holds
for b being Element of E st b ^2 = a holds
( FAdj (F,{b}) is SplittingField of X^2- a & deg ((FAdj (F,{b})),F) = 2 )

proof end;

unique20: for F1, F2 being Field st F1 is Subfield of F2 & F2 is Subfield of F1 holds
for f being Function of F1,F2 st f = id F1 holds
f is isomorphism

proof end;

theorem :: FIELD_9:72

for F being non 2 -characteristic Field
for E being FieldExtension of F holds
( deg (E,F) = 2 iff ex a being Element of F st
( ( for b being Element of F holds not a = b ^2 ) & ex b being Element of E st
( a = b ^2 & E == FAdj (F,{b}) ) ) )

proof end;

theorem :: FIELD_9:73

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for E being FieldExtension of F holds
( E is F -quadratic iff ex a being non square Element of F st E, FAdj (F,{(sqrt a)}) are_isomorphic_over F )

proof end;