:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller
::
:: 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 b1 -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;
existence
ex b1 being Element of S st
( not b1 is zero & b1 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
existence
ex b1 being Field st
( not b1 is 2 -characteristic & b1 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;

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
existence
not for b1 being polynomial_disjoint Field holds b1 is algebraic-closed
proof end;
end;

registration
let F be non algebraic-closed Field;
existence
ex b1 being Element of the carrier of () st
( b1 is irreducible & not b1 is linear )
proof end;
end;

registration
let F be Field;
cluster irreducible non linear -> non with_roots for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 is irreducible & not b1 is linear holds
not b1 is with_roots
;
cluster irreducible with_roots -> linear for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 is irreducible & b1 is with_roots holds
b1 is linear
;
end;

registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of ();
coherence
proof end;
end;

registration
let F be non algebraic-closed polynomial_disjoint Field;
let p be irreducible non linear Element of the carrier of ();
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 b1 -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 () equals :: FIELD_9:def 2
rpoly (1,a);
coherence
rpoly (1,a) is Element of the carrier of ()
by POLYNOM3:def 10;
func X+ a -> Element of the carrier of () equals :: FIELD_9:def 3
rpoly (1,(- a));
coherence
rpoly (1,(- a)) is Element of the carrier of ()
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;
coherence
( X- a is linear & X- a is monic )
proof end;
coherence
( X+ a is linear & X+ a is monic )
proof end;
end;

definition
let R be Ring;
let p be Polynomial of R;
deg p = 2;
end;

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;
existence
ex b1 being Polynomial of R st
( b1 is monic & b1 is quadratic )
proof end;
existence
ex b1 being Element of the carrier of () st
( b1 is monic & b1 is quadratic )
proof end;
end;

registration
let R be non degenerated Ring;
coherence
for b1 being quadratic Polynomial of R holds not b1 is constant
proof end;
cluster quadratic -> non constant quadratic for Element of the carrier of ();
coherence
for b1 being quadratic Element of the carrier of () holds not b1 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;
coherence
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
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
;
end;

registration
let R be non degenerated Ring;
existence
ex b1 being Polynomial of R st
( b1 is monic & b1 is purely_quadratic )
proof end;
end;

registration
let R be non degenerated Ring;
coherence
for b1 being Polynomial of R st b1 is purely_quadratic holds
;
end;

definition
let R be Ring;
let a be Element of R;
func X^2- a -> Element of the carrier of () equals :: FIELD_9:def 7
<%(- a),(0. R),(1. R)%>;
coherence
<%(- a),(0. R),(1. R)%> is Element of the carrier of ()
by POLYNOM3:def 10;
func X^2+ a -> Element of the carrier of () equals :: FIELD_9:def 8
<%a,(0. R),(1. R)%>;
coherence
<%a,(0. R),(1. R)%> is Element of the carrier of ()
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 b1 being Polynomial of R st b1 is linear holds
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 b1 being Polynomial of R st b1 is quadratic holds
not b1 is linear
;
end;

registration
let R be non degenerated Ring;
let a be Element of R;
coherence
( X^2- a is purely_quadratic & X^2- a is monic & not X^2- a is constant )
;
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 b1 being Element of R ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b1 = (b ^2) - ((4 '*' a) * c) )
proof end;
uniqueness
for b1, b2 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%> & b1 = (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%> & b2 = (b ^2) - ((4 '*' a) * c) ) holds
b1 = b2
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 b3 being Element of R holds
( b3 = Discriminant p iff ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b3 = (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 b1 being Element of R holds
( b1 = Discriminant p iff ex b, c being Element of R st
( p = <%c,b,(1. R)%> & b1 = (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 b3 being Element of R holds
( b3 = Discriminant p iff ex b, c being Element of R st
( p = <%c,b,(1. R)%> & b3 = (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 b1 being Element of R holds
( b1 = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b1 = - (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 b3 being Element of R holds
( b3 = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b3 = - (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 () = 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 () = 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 () 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 ;

registration
coherence
proof end;
end;

registration
cluster -> square for Element of the carrier of (Z/ 2);
coherence
for b1 being Element of (Z/ 2) holds b1 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 b1 being non zero Polynomial of (Z/ 2) holds b1 is monic
proof end;
cluster non zero -> non zero monic for Element of the carrier of (Polynom-Ring (Z/ 2));
coherence
for b1 being non zero Element of the carrier of (Polynom-Ring (Z/ 2)) holds b1 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 } =
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
proof end;

registration
coherence
not X^2 is irreducible
by z21;
coherence
not X^2+1 is irreducible
by z22;
coherence
not X^2+X is irreducible
by z23;
coherence
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
coherence ;
end;

:: deftheorem defines alpha FIELD_9:def 18 :

definition
func alpha-1 -> Element of () equals :: FIELD_9:def 19
alpha - (1. ());
coherence
alpha - (1. ()) is Element of ()
;
end;

:: deftheorem defines alpha-1 FIELD_9:def 19 :
alpha-1 = alpha - (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 " = - (alpha + (1. ())) & - alpha = () + (1. ()) )
proof end;

theorem lemalph: :: FIELD_9:46
proof end;

theorem :: FIELD_9:47
( X^2+X+1 = () *' (X- ()) & () *' (X- ()) = () *' () ) by ;

theorem lemZ2roots: :: FIELD_9:48
proof end;

theorem :: FIELD_9:49
card (Roots ((FAdj ((Z/ 2),)),X^2+X+1)) = 2 by ;

theorem lemZ2min: :: FIELD_9:50
MinPoly (alpha,(Z/ 2)) = X^2+X+1
proof end;

theorem :: FIELD_9:51
deg ((FAdj ((Z/ 2),)),(Z/ 2)) = 2
proof end;

theorem :: FIELD_9:52
FAdj ((Z/ 2),) 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 - () -> non square ;
coherence
not - () is being_a_square
proof end;
cluster - () -> non square ;
coherence
not - () is being_a_square
proof end;
end;

registration
coherence
for b1 being non degenerated Ring st b1 is algebraic-closed holds
proof end;
coherence
for b1 being non degenerated Ring st b1 is preordered holds
proof end;
end;

registration
coherence ;
coherence ;
coherence ;
end;

registration
existence
ex b1 being Field st
( not b1 is quadratic_complete & b1 is polynomial_disjoint & b1 is strict )
proof end;
existence
ex b1 being Field st
( b1 is quadratic_complete & b1 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 b1 being Ring st not b1 is quadratic_complete holds
not b1 is degenerated
proof end;
end;

registration
let R be non quadratic_complete Ring;
existence
not for b1 being Element of R holds b1 is square
proof end;
end;

registration
existence
ex b1 being Field st
( b1 is strict & b1 is polynomial_disjoint & not b1 is quadratic_complete & not b1 is 2 -characteristic )
proof end;
end;

registration
let F be non 2 -characteristic non quadratic_complete Field;
existence
ex b1 being Element of the carrier of () st
( b1 is monic & b1 is quadratic & b1 is irreducible )
proof end;
end;

registration
let F be non 2 -characteristic Field;
let a be square Element of F;
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;
coherence 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 b1 -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 b1 -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 b1 -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 ();
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 () holds
( p is DC-square iff DC p is square );

registration
let F be non 2 -characteristic Field;
existence
ex b1 being quadratic Element of the carrier of () st
( b1 is monic & b1 is DC-square )
proof end;
end;

registration
let F be non 2 -characteristic non quadratic_complete Field;
existence
ex b1 being quadratic Element of the carrier of () st
( b1 is monic & not b1 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 ();
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 ();
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 ();
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 () 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 ();
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 ();
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 () 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 ();
func Root1 p -> Element of (FAdj (F,{(sqrt (DC p))})) equals :: FIELD_9:def 24
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) + ()) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");
coherence
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC 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))}))))) - ()) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");
coherence
((- (@ ((p . 1),(FAdj (F,{(sqrt (DC 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 () holds Root1 p = ((- (@ ((p . 1),(FAdj (F,{(sqrt (DC 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 () holds Root2 p = ((- (@ ((p . 1),(FAdj (F,{(sqrt (DC 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 () holds () * () = 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 ()
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) + ()) * ((2 '*' a) ") & Root2 p = ((- b) - ()) * ((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 () holds p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- ()) *' (X- ()))
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 () holds Roots ((FAdj (F,{(sqrt (DC p))})),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 () 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 () 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 () 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;
existence
ex b1 being FieldExtension of F st b1 is F -quadratic
proof end;
end;

registration
let F be Field;
coherence
for b1 being FieldExtension of F st b1 is F -quadratic holds
b1 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;
coherence
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;