:: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller

::

:: Received November 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

definition

let R be Ring;

let S be RingExtension of R;

let a be R -membered Element of S;

coherence

a is Element of R by FIELD_7:def 5;

end;
let S be RingExtension of R;

let a be R -membered Element of S;

coherence

a is Element of R by FIELD_7:def 5;

:: deftheorem defines @ FIELD_9:def 1 :

for R being Ring

for S being RingExtension of R

for a being b_{1} -membered Element of S holds @ a = a;

for R being Ring

for S being RingExtension of R

for a being b

registration

let R be Ring;

let S be RingExtension of R;

let a be R -membered Element of S;

coherence

- a is R -membered

end;
let S be RingExtension of R;

let a be R -membered Element of S;

coherence

- a is R -membered

proof end;

registration

let R be Ring;

let S be RingExtension of R;

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

coherence

a + b is R -membered

a * b is R -membered

end;
let S be RingExtension of R;

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

coherence

a + b is R -membered

proof end;

coherence a * b is R -membered

proof end;

registration
end;

registration

let R be non degenerated Ring;

let S be RingExtension of R;

coherence

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

end;
let S be RingExtension of R;

coherence

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

proof end;

registration

let R be non degenerated Ring;

let S be RingExtension of R;

ex b_{1} being Element of S st

( not b_{1} is zero & b_{1} is R -membered )

end;
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

( not b

proof end;

registration

let F be Field;

let E be FieldExtension of F;

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

coherence

a " is F -membered

end;
let E be FieldExtension of F;

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

coherence

a " is F -membered

proof end;

registration

let R be Ring;

let a, b, c be Element of R;

coherence

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

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

coherence

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

proof end;

registration

ex b_{1} being Field st

( not b_{1} is 2 -characteristic & b_{1} is strict )
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() non 2 -characteristic for doubleLoopStr ;

existence ex b

( not b

proof end;

registration

let R be Ring;

reducibility

(0. R) ^2 = 0. R

(1. R) ^2 = 1. R

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

end;
reducibility

(0. R) ^2 = 0. R

proof end;

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

proof end;

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

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 ")

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)

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 )

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 )

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

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 )

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})

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)})

for E being FieldExtension of F

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

proof end;

registration

not for b_{1} being polynomial_disjoint Field holds b_{1} is algebraic-closed
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 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

proof end;

registration

let F be non algebraic-closed Field;

ex b_{1} being Element of the carrier of (Polynom-Ring F) st

( b_{1} is irreducible & not b_{1} is linear )

end;
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

( b

proof end;

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is irreducible & not b_{1} is linear holds

not b_{1} is with_roots
;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is irreducible & b_{1} is with_roots holds

b_{1} is linear
;

end;
coherence

for b

not b

coherence

for b

b

registration

let F be polynomial_disjoint Field;

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

coherence

KrRootP p is F -algebraic

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

coherence

KrRootP p is F -algebraic

proof 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);

coherence

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

end;
let p be irreducible non linear Element of the carrier of (Polynom-Ring F);

coherence

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

proof 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)

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;

coherence

rpoly (k,a) is monic

end;
let k be non zero Element of NAT ;

let a be Element of L;

coherence

rpoly (k,a) is monic

proof end;

registration

let R be non degenerated Ring;

let a be non zero Element of R;

let b be Element of R;

coherence

<%b,a%> is linear

end;
let a be non zero Element of R;

let b be Element of R;

coherence

<%b,a%> is linear

proof end;

registration

let R be non degenerated Ring;

let b be Element of R;

coherence

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

end;
let b be Element of R;

coherence

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

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%>

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)

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_{1} -membered Element of E st Ext_eval (p,a) = y + (a * z)

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

proof end;

definition

let R be Ring;

let a be Element of R;

coherence

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

coherence

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

end;
let a be Element of R;

coherence

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

coherence

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

:: deftheorem defines X- FIELD_9:def 2 :

for R being Ring

for a being Element of R holds X- a = rpoly (1,a);

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));

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 )

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

end;
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;

:: 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 );

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;

ex b_{1} being Polynomial of R st

( b_{1} is monic & b_{1} is quadratic )

ex b_{1} being Element of the carrier of (Polynom-Ring R) st

( b_{1} is monic & b_{1} is quadratic )

end;
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

( b

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

( b

proof end;

registration

let R be non degenerated Ring;

for b_{1} being quadratic Polynomial of R holds not b_{1} is constant

for b_{1} being quadratic Element of the carrier of (Polynom-Ring R) holds not b_{1} is constant

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

coherence for b

proof end;

coherence for b

proof end;

definition

let L be non empty ZeroStr ;

let a, b, c be Element of L;

correctness

coherence

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

;

end;
let a, b, c be Element of L;

correctness

coherence

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

;

:: 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);

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;

coherence

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

end;
let a, b, c be Element of L;

coherence

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

proof end;

theorem :: FIELD_9:16

qua2: for L being non empty ZeroStr

for a, b, c being Element of L holds len <%c,b,a%> <= 3

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 )

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

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

end;
let a be non zero Element of R;

let b, c be Element of R;

coherence

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

registration

let R be non degenerated Ring;

let b, c be Element of R;

coherence

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

end;
let b, c be Element of R;

coherence

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

proof end;

registration

let R be domRing;

let a, x be non zero Element of R;

let b, c be Element of R;

coherence

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

end;
let a, x be non zero Element of R;

let b, c be Element of R;

coherence

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

proof 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)%>

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))

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%> )

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)%> )

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%>

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;

end;
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%>;

ex a being non zero Element of R ex c being Element of R st p = <%c,(0. R),a%>;

:: 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%> );

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;

coherence

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

end;
let a be non zero Element of R;

let c be Element of R;

coherence

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

registration

let R be non degenerated Ring;

ex b_{1} being Polynomial of R st

( b_{1} is monic & b_{1} is purely_quadratic )

end;
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

( b

proof end;

registration

let R be non degenerated Ring;

for b_{1} being Polynomial of R st b_{1} is purely_quadratic holds

b_{1} is quadratic
;

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

coherence for b

b

definition

let R be Ring;

let a be Element of R;

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

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

end;
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)%>;

<%(- 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)%>;

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

:: 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)%>;

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)%>;

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;

for b_{1} being Polynomial of R st b_{1} is linear holds

not b_{1} is quadratic
by FIELD_5:def 1;

for b_{1} being Polynomial of R st b_{1} is quadratic holds

not b_{1} is linear
;

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

coherence for b

not b

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

coherence for b

not b

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;
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 ) ;

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)%>

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 )

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

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) "))}

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))

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;

ex b_{1} 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_{1} = (b ^2) - ((4 '*' a) * c) )

for b_{1}, b_{2} 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_{1} = (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_{2} = (b ^2) - ((4 '*' a) * c) ) holds

b_{1} = b_{2}

end;
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 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) );

ex b

( p = <%c,b,a%> & b

proof end;

uniqueness for b

( p = <%c,b,a%> & b

( p = <%c,b,a%> & b

b

proof end;

:: deftheorem defDC defines Discriminant FIELD_9:def 9 :

for R being non degenerated Ring

for p being quadratic Polynomial of R

for b_{3} being Element of R holds

( b_{3} = Discriminant p iff ex a being non zero Element of R ex b, c being Element of R st

( p = <%c,b,a%> & b_{3} = (b ^2) - ((4 '*' a) * c) ) );

for R being non degenerated Ring

for p being quadratic Polynomial of R

for b

( b

( p = <%c,b,a%> & b

notation
end;

definition

let R be non degenerated Ring;

let p be monic quadratic Polynomial of R;

for b_{1} being Element of R holds

( b_{1} = Discriminant p iff ex b, c being Element of R st

( p = <%c,b,(1. R)%> & b_{1} = (b ^2) - (4 '*' c) ) )

end;
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 ex b, c being Element of R st

( p = <%c,b,(1. R)%> & it = (b ^2) - (4 '*' c) );

for b

( b

( p = <%c,b,(1. R)%> & b

proof 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_{3} being Element of R holds

( b_{3} = Discriminant p iff ex b, c being Element of R st

( p = <%c,b,(1. R)%> & b_{3} = (b ^2) - (4 '*' c) ) );

for R being non degenerated Ring

for p being monic quadratic Polynomial of R

for b

( b

( p = <%c,b,(1. R)%> & b

definition

let R be non degenerated Ring;

let p be monic purely_quadratic Polynomial of R;

for b_{1} being Element of R holds

( b_{1} = Discriminant p iff ex c being Element of R st

( p = <%c,(0. R),(1. R)%> & b_{1} = - (4 '*' c) ) )

end;
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 ex c being Element of R st

( p = <%c,(0. R),(1. R)%> & it = - (4 '*' c) );

for b

( b

( p = <%c,(0. R),(1. R)%> & b

proof 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_{3} being Element of R holds

( b_{3} = Discriminant p iff ex c being Element of R st

( p = <%c,(0. R),(1. R)%> & b_{3} = - (4 '*' c) ) );

for R being non degenerated Ring

for p being monic purely_quadratic Polynomial of R

for b

( b

( p = <%c,(0. R),(1. R)%> & b

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 )

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 )

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 ) )

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 )

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 )

for a being Element of F holds

( X^2- a is reducible iff a is square )

proof end;

registration
end;

registration

for b_{1} being non zero Polynomial of (Z/ 2) holds b_{1} is monic

for b_{1} being non zero Element of the carrier of (Polynom-Ring (Z/ 2)) holds b_{1} is monic
;

end;

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

proof end;

coherence for b

definition

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

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

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

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

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

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

end;

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))%>;

<%(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))%>;

<%(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))%>;

<%(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))%>;

<%(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))%>;

<%(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))%>;

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

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

X^2+X+1 is irreducible

end;
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

X^2+X+1 is irreducible

proof 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;

definition

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

end;

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)));

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

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 :: FIELD_9:47

theorem :: FIELD_9:49

:: 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 );

for R being Ring holds

( R is quadratic_complete iff the carrier of R c= SQ R );

registration

coherence

not - (1. F_Real) is being_a_square

not - (1. F_Rat) is being_a_square

end;
not - (1. F_Real) is being_a_square

proof end;

coherence not - (1. F_Rat) is being_a_square

proof end;

registration

for b_{1} being non degenerated Ring st b_{1} is algebraic-closed holds

b_{1} is quadratic_complete

for b_{1} being non degenerated Ring st b_{1} is preordered holds

not b_{1} is quadratic_complete
end;

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

b

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

not b

proof end;

registration

coherence

not F_Rat is quadratic_complete ;

coherence

not F_Real is quadratic_complete ;

coherence

F_Complex is quadratic_complete ;

end;
not F_Rat is quadratic_complete ;

coherence

not F_Real is quadratic_complete ;

coherence

F_Complex is quadratic_complete ;

registration

ex b_{1} being Field st

( not b_{1} is quadratic_complete & b_{1} is polynomial_disjoint & b_{1} is strict )

ex b_{1} being Field st

( b_{1} is quadratic_complete & b_{1} is strict )
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() polynomial_disjoint non quadratic_complete for doubleLoopStr ;

existence ex b

( not b

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

( b

proof end;

registration

for b_{1} being Ring st not b_{1} is quadratic_complete holds

not b_{1} is degenerated
end;

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

coherence for b

not b

proof end;

registration

let R be non quadratic_complete Ring;

not for b_{1} being Element of R holds b_{1} is square

end;
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

proof end;

registration

ex b_{1} being Field st

( b_{1} is strict & b_{1} is polynomial_disjoint & not b_{1} is quadratic_complete & not b_{1} is 2 -characteristic )
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() non 2 -characteristic polynomial_disjoint non quadratic_complete for doubleLoopStr ;

existence ex b

( b

proof end;

registration

let F be non 2 -characteristic non quadratic_complete Field;

ex b_{1} being Element of the carrier of (Polynom-Ring F) st

( b_{1} is monic & b_{1} is quadratic & b_{1} is irreducible )

end;
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

( b

proof 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;
let a be square Element of F;

coherence

not X^2- a is irreducible by naH2;

registration

let F be non 2 -characteristic non quadratic_complete Field;

let a be non square Element of F;

coherence

X^2- a is irreducible by naH2;

end;
let a be non square Element of F;

coherence

X^2- a is irreducible by naH2;

definition

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

let a be non square Element of F;

coherence

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

end;
let a be non square Element of F;

coherence

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

:: 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);

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;

coherence

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

end;
let a be non square Element of F;

coherence

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

proof end;

registration

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

let a be non square Element of F;

coherence

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

end;
let a be non square Element of F;

coherence

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

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;

coherence

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

end;
let a be non square Element of F;

coherence

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

proof 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

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;

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;

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

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))}

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

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))

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

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_{1} -membered Element of (FAdj (F,{(sqrt a)})) : verum }

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

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_{1} -membered Element of (FAdj (F,{(sqrt a)})) st a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) holds

( a1 = a2 & b1 = b2 )

for a being non square Element of F

for a1, a2, b1, b2 being b

( a1 = a2 & b1 = b2 )

proof end;

definition
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 );

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;

ex b_{1} being quadratic Element of the carrier of (Polynom-Ring F) st

( b_{1} is monic & b_{1} is DC-square )

end;
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

( b

proof end;

registration

let F be non 2 -characteristic non quadratic_complete Field;

ex b_{1} being quadratic Element of the carrier of (Polynom-Ring F) st

( b_{1} is monic & not b_{1} is DC-square )

end;
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

( b

proof 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);

coherence

not DC p is being_a_square by defDCps;

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

coherence

not DC p is being_a_square by defDCps;

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);

coherence

X^2- (DC p) is irreducible ;

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

coherence

X^2- (DC p) is irreducible ;

registration

let F be non 2 -characteristic Field;

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

coherence

not X^2- (DC p) is irreducible

end;
let p be quadratic DC-square Element of the carrier of (Polynom-Ring F);

coherence

not X^2- (DC p) is irreducible

proof 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 )

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);

coherence

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

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

coherence

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

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);

coherence

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

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

coherence

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

proof 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);

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);

((- (@ ((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))})) ;

((- (@ ((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;
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))}))))) ");

((- (@ ((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))}))))) ");

((- (@ ((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))})) ;

:: 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))}))))) ");

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))}))))) ");

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

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) ") )

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)))

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)}

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

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;

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

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;

:: 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 );

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;

ex b_{1} being FieldExtension of F st b_{1} is F -quadratic

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 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

proof end;

registration

let F be Field;

for b_{1} being FieldExtension of F st b_{1} is F -quadratic holds

b_{1} is F -finite

end;
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

b

proof end;

registration

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

let a be non square Element of F;

coherence

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

end;
let a be non square Element of F;

coherence

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

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 )

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}) ) ) )

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 )

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;