:: Splitting Fields for the Rational Polynomials X^2-2, X^2+X+1, X^3-1, and X^3-2
:: by Christoph Schwarzweller and Sara Burgoa
::
:: Received April 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

definition

let L be non empty doubleLoopStr ;
let a, b, c be Element of L;
:: original: {
redefine func {a,b,c} -> Subset of L;
coherence
{a,b,c} is Subset of L

proof end;

end;

registration

let i be Integer;

cluster i |^ 3 -> integer ;

coherence
i |^ 3 is integer

proof end;

end;

registration

let i be even Integer;

cluster i |^ 3 -> even ;

coherence
i |^ 3 is even

proof end;

end;

registration

let i be odd Integer;

cluster i |^ 3 -> odd ;

coherence
not i |^ 3 is even

proof end;

end;

theorem lemcontr2: :: FIELD_10:1

for r, s being Complex holds (r * s) |^ 3 = (r |^ 3) * (s |^ 3)

proof end;

theorem lemcontr1: :: FIELD_10:2

for r being Rational holds
( r |^ 3 >= 0 iff r >= 0 )

proof end;

theorem lemcontr: :: FIELD_10:3

for r being Rational holds not r |^ 3 = 2

proof end;

registration

cluster 3 -Root 2 -> non rational ;

coherence
not 3 -Root 2 is rational

proof end;

end;

theorem lemfinset: :: FIELD_10:4

for X1, X2 being finite set st X1 c= X2 & card X1 = card X2 holds
X1 = X2

proof end;

registration

let F be Field;

cluster Relation-like NAT -defined the carrier of F -valued Function-like quasi_total finite-Support 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 linear

proof end;

cluster Relation-like NAT -defined the carrier of F -valued Function-like quasi_total finite-Support non constant non linear for Element of the carrier of (Polynom-Ring F);

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

proof end;

end;

theorem thirred2: :: FIELD_10:5

for F being Field
for p being Element of the carrier of (Polynom-Ring F) st deg p = 2 holds
( p is reducible iff p is with_roots )

proof end;

theorem thirred: :: FIELD_10:6

for F being Field
for p being Element of the carrier of (Polynom-Ring F) st deg p = 3 holds
( p is reducible iff p is with_roots )

proof end;

registration

cluster F_Complex -> F_Rat -extending ;

coherence
F_Complex is F_Rat -extending ;

end;

registration

cluster complex real ext-real F_Rat -membered for Element of the carrier of F_Real;

existence
ex b₁ being Element of F_Real st b₁ is F_Rat -membered

proof end;

cluster complex real ext-real non F_Rat -membered for Element of the carrier of F_Real;

existence
not for b₁ being Element of F_Real holds b₁ is F_Rat -membered

proof end;

cluster complex F_Real -membered for Element of the carrier of F_Complex;

existence
ex b₁ being Element of F_Complex st b₁ is F_Real -membered

proof end;

cluster complex non F_Real -membered for Element of the carrier of F_Complex;

existence
not for b₁ being Element of F_Complex holds b₁ is F_Real -membered

proof end;

cluster complex F_Rat -membered for Element of the carrier of F_Complex;

existence
ex b₁ being Element of F_Complex st b₁ is F_Rat -membered

proof end;

cluster complex non F_Rat -membered for Element of the carrier of F_Complex;

existence
not for b₁ being Element of F_Complex holds b₁ is F_Rat -membered

proof end;

end;

theorem mmo: :: FIELD_10:7

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
Roots (K,p) = Roots (K,q)

proof end;

bb0: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of E
for b being Element of K st b = a holds
the carrier of (RAdj (F,{a})) = the carrier of (RAdj (F,{b}))

proof end;

theorem bb1: :: FIELD_10:8

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of E
for b being Element of K st b = a holds
RAdj (F,{a}) = RAdj (F,{b})

proof end;

bba: for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being b₁ -algebraic Element of E
for b being b₁ -algebraic Element of K st b = a holds
the carrier of (FAdj (F,{a})) = the carrier of (FAdj (F,{b}))

proof end;

theorem mmk: :: FIELD_10:9

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being b₁ -algebraic Element of E
for b being b₁ -algebraic Element of K st b = a holds
FAdj (F,{a}) = FAdj (F,{b})

proof end;

theorem mmv: :: FIELD_10:10

for F being Field
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for a being b₁ -algebraic Element of E
for b being b₁ -algebraic Element of K st a = b holds
MinPoly (a,F) = MinPoly (b,F)

proof end;

theorem mmu: :: FIELD_10:11

for F being Field
for E being b₁ -finite FieldExtension of F
for a being Element of E holds deg (MinPoly (a,F)) divides deg (E,F)

proof end;

registration

let F be Field;
let E be FieldExtension of F;
let T1, T2 be Subset of E;

cluster FieldAdjunction (F,(T1 \/ T2)) -> FAdj (F,T1) -extending FAdj (F,T2) -extending ;

coherence
( FAdj (F,(T1 \/ T2)) is FAdj (F,T1) -extending & FAdj (F,(T1 \/ T2)) is FAdj (F,T2) -extending )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a, b be Element of E;

cluster FieldAdjunction (F,{a,b}) -> FAdj (F,{a}) -extending FAdj (F,{b}) -extending ;

coherence
( FAdj (F,{a,b}) is FAdj (F,{a}) -extending & FAdj (F,{a,b}) is FAdj (F,{b}) -extending )

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let a, b, c be Element of E;

cluster FieldAdjunction (F,{a,b,c}) -> FAdj (F,{a,b}) -extending FAdj (F,{a,c}) -extending FAdj (F,{b,c}) -extending ;

coherence
( FAdj (F,{a,b,c}) is FAdj (F,{a,b}) -extending & FAdj (F,{a,b,c}) is FAdj (F,{a,c}) -extending & FAdj (F,{a,b,c}) is FAdj (F,{b,c}) -extending )

proof end;

end;

LL0: ( (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 0 = - 2 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 1 = 0 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 2 = 0 & (((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . 3 = 1 & ( for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 2))) +* (3,1)) . n = 0 ) )

proof end;

lemI: for z being Element of F_Complex holds
( z |^ 3 = z * (z ^2) & z |^ 2 = z ^2 & z |^ 2 = z * z )

proof end;

LL01: ( (((0_. F_Rat) +* (0,(- 1))) +* (3,1)) . 0 = - 1 & (((0_. F_Rat) +* (0,(- 1))) +* (3,1)) . 1 = 0 & (((0_. F_Rat) +* (0,(- 1))) +* (3,1)) . 2 = 0 & (((0_. F_Rat) +* (0,(- 1))) +* (3,1)) . 3 = 1 & ( for n being Nat st n >= 4 holds
(((0_. F_Rat) +* (0,(- 1))) +* (3,1)) . n = 0 ) )

proof end;

definition

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

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

func X^3-1 -> Element of the carrier of (Polynom-Ring F_Rat) equals :: FIELD_10:def 2
((0_. F_Rat) +* (0,(- 1))) +* (3,1);

coherence
((0_. F_Rat) +* (0,(- 1))) +* (3,1) is Element of the carrier of (Polynom-Ring F_Rat)

proof end;

func X^3-2 -> Element of the carrier of (Polynom-Ring F_Rat) equals :: FIELD_10:def 3
((0_. F_Rat) +* (0,(- 2))) +* (3,1);

coherence
((0_. F_Rat) +* (0,(- 2))) +* (3,1) is Element of the carrier of (Polynom-Ring F_Rat)

proof end;

func X^2+X+1 -> Element of the carrier of (Polynom-Ring F_Rat) equals :: FIELD_10:def 4
<%(1. F_Rat),(1. F_Rat),(1. F_Rat)%>;

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

end;

:: deftheorem defines X^2-2 FIELD_10:def 1 :
X^2-2 = <%(- ((1. F_Rat) + (1. F_Rat))),(0. F_Rat),(1. F_Rat)%>;

:: deftheorem defines X^3-1 FIELD_10:def 2 :
X^3-1 = ((0_. F_Rat) +* (0,(- 1))) +* (3,1);

:: deftheorem defines X^3-2 FIELD_10:def 3 :
X^3-2 = ((0_. F_Rat) +* (0,(- 2))) +* (3,1);

:: deftheorem defines X^2+X+1 FIELD_10:def 4 :
X^2+X+1 = <%(1. F_Rat),(1. F_Rat),(1. F_Rat)%>;

definition

func 2-Root(2) -> non zero Element of F_Real equals :: FIELD_10:def 5
sqrt 2;

coherence
sqrt 2 is non zero Element of F_Real

proof end;

func 3-Root(2) -> non zero Element of F_Real equals :: FIELD_10:def 6
3 -Root 2;

coherence
3 -Root 2 is non zero Element of F_Real

proof end;

func 2-CRoot(2) -> non zero Element of F_Complex equals :: FIELD_10:def 7
sqrt 2;

coherence
sqrt 2 is non zero Element of F_Complex

proof end;

func 3-CRoot(2) -> non zero Element of F_Complex equals :: FIELD_10:def 8
3 -Root 2;

coherence
3 -Root 2 is non zero Element of F_Complex

proof end;

func sqrt(-3) -> non zero Element of F_Complex equals :: FIELD_10:def 9
<i> * (sqrt 3);

coherence
<i> * (sqrt 3) is non zero Element of F_Complex

proof end;

func zeta -> non zero Element of F_Complex equals :: FIELD_10:def 10
((- 1) + (<i> * (sqrt 3))) / 2;

coherence
((- 1) + (<i> * (sqrt 3))) / 2 is non zero Element of F_Complex

proof end;

end;

:: deftheorem defines 2-Root(2) FIELD_10:def 5 :
2-Root(2) = sqrt 2;

:: deftheorem defines 3-Root(2) FIELD_10:def 6 :
3-Root(2) = 3 -Root 2;

:: deftheorem defines 2-CRoot(2) FIELD_10:def 7 :
2-CRoot(2) = sqrt 2;

:: deftheorem defines 3-CRoot(2) FIELD_10:def 8 :
3-CRoot(2) = 3 -Root 2;

:: deftheorem defines sqrt(-3) FIELD_10:def 9 :
sqrt(-3) = <i> * (sqrt 3);

:: deftheorem defines zeta FIELD_10:def 10 :
zeta = ((- 1) + (<i> * (sqrt 3))) / 2;

LL1: ( len X^3-2 = 4 & len X^3-1 = 4 )

proof end;

LL: ( deg X^3-2 = 3 & deg X^3-1 = 3 & deg X^2+X+1 = 2 & deg X^2-2 = 2 )

proof end;

LL3: for x being Element of F_Rat holds eval (X^3-2,x) = (x |^ 3) - 2

proof end;

LL31: for x being Element of F_Rat holds eval (X^3-1,x) = (x |^ 3) - 1

proof end;

LL32: for x being Element of F_Rat holds eval (X^2+X+1,x) = ((x |^ 2) + x) + 1

proof end;

LKX2: for x being Element of F_Rat holds eval (X^2-2,x) = (x |^ 2) - 2

proof end;

LKX2ext: for z being Element of F_Real holds Ext_eval (X^2-2,z) = (z |^ 2) - 2

proof end;

lem3: for r being Rational
for a being Element of F_Rat st a = r holds
a |^ 3 = r |^ 3

proof end;

R32: 3-Root(2) |^ 3 = 2

proof end;

LL2: Ext_eval (X^3-2,3-Root(2)) = 0. F_Real

proof end;

LZ23: ( zeta |^ 2 <> 1 & zeta |^ 3 = 1 & zeta |^ 2 = (- zeta) - 1 )

proof end;

lem3c: for r being Complex
for a being Element of F_Complex st a = r holds
a |^ 3 = r |^ 3

proof end;

LL33: Ext_eval (X^3-1,zeta) = 0. F_Complex

proof end;

evalext11: for z being Element of F_Complex holds Ext_eval (X^2+X+1,z) = ((z |^ 2) + z) + 1

proof end;

rootz: Roots (F_Complex,X^2+X+1) = {zeta,(zeta ^2)}

proof end;

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

proof end;

lemX3: X^3-1 = (X- (1. F_Rat)) * X^2+X+1

proof end;

evalext1: for z being Element of F_Complex holds Ext_eval (X^3-1,z) = (z |^ 3) - 1

proof end;

lemCRo: for z being Element of the carrier of F_Complex holds
( Ext_eval (X^3-1,z) = 0. F_Complex iff z is CRoot of 3,1 )

proof end;

lemCRo2: ( zeta is CRoot of 3,1 & zeta ^2 is CRoot of 3,1 )

proof end;

lemroots3: Roots (F_Complex,X^3-1) = {1,zeta,(zeta ^2)}

proof end;

lemlem: ( not zeta in REAL & not zeta ^2 in REAL )

proof end;

registration

cluster X^2-2 -> monic irreducible purely_quadratic ;

coherence
( X^2-2 is monic & X^2-2 is purely_quadratic & X^2-2 is irreducible )

proof end;

cluster X^3-2 -> monic irreducible non constant ;

coherence
( X^3-2 is monic & not X^3-2 is constant & X^3-2 is irreducible )

proof end;

cluster X^3-1 -> monic reducible non constant ;

coherence
( X^3-1 is monic & not X^3-1 is constant & not X^3-1 is irreducible )

proof end;

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

coherence
( X^2+X+1 is monic & X^2+X+1 is quadratic & X^2+X+1 is irreducible )

proof end;

end;

registration

cluster 2-Root(2) -> non zero F_Rat -algebraic non F_Rat -membered ;

coherence
( not 2-Root(2) is F_Rat -membered & 2-Root(2) is F_Rat -algebraic )

proof end;

cluster 2-CRoot(2) -> non zero F_Rat -algebraic non F_Rat -membered ;

coherence
( not 2-CRoot(2) is F_Rat -membered & 2-CRoot(2) is F_Rat -algebraic )

proof end;

cluster 3-Root(2) -> non zero F_Rat -algebraic non F_Rat -membered ;

coherence
( not 3-Root(2) is F_Rat -membered & 3-Root(2) is F_Rat -algebraic )

proof end;

cluster 3-CRoot(2) -> non zero F_Rat -algebraic non F_Rat -membered ;

coherence
( not 3-CRoot(2) is F_Rat -membered & 3-CRoot(2) is F_Rat -algebraic )

proof end;

cluster zeta -> non zero F_Rat -algebraic non F_Real -membered ;

coherence
( not zeta is F_Real -membered & zeta is F_Rat -algebraic )

proof end;

cluster zeta ^2 -> F_Rat -algebraic non F_Real -membered ;

coherence
( not zeta ^2 is F_Real -membered & zeta ^2 is F_Rat -algebraic )

proof end;

end;

registration

cluster FieldAdjunction (F_Rat,{3-Root(2)}) -> F_Rat -finite ;

coherence
FAdj (F_Rat,{3-Root(2)}) is F_Rat -finite ;

cluster FieldAdjunction (F_Rat,{3-CRoot(2),zeta}) -> F_Rat -finite ;

coherence
FAdj (F_Rat,{3-CRoot(2),zeta}) is F_Rat -finite ;

end;

llsplit1: for F being Field st F is algebraic-closed holds
for p being non constant Polynomial of F holds p splits_in F

proof end;

LLsplit: ( X^3-2 splits_in F_Complex & X^3-1 splits_in F_Complex & X^2+X+1 splits_in F_Complex )

proof end;

registration

cluster F_Real -> FAdj (F_Rat,{2-Root(2)}) -extending ;

coherence
F_Real is FAdj (F_Rat,{2-Root(2)}) -extending by FIELD_4:7;

cluster F_Real -> FAdj (F_Rat,{3-Root(2)}) -extending ;

coherence
F_Real is FAdj (F_Rat,{3-Root(2)}) -extending by FIELD_4:7;

cluster F_Complex -> FAdj (F_Rat,{2-Root(2)}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{2-Root(2)}) -extending ;

cluster F_Complex -> FAdj (F_Rat,{3-Root(2)}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{3-Root(2)}) -extending ;

cluster F_Complex -> FAdj (F_Rat,{3-CRoot(2),zeta}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{3-CRoot(2),zeta}) -extending by FIELD_4:7;

end;

theorem :: FIELD_10:12

zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;

theorem :: FIELD_10:13

zeta ^2 = (- (1 / 2)) - ((<i> * (sqrt 3)) / 2)

proof end;

theorem :: FIELD_10:14

( zeta |^ 2 <> 1 & zeta |^ 3 = 1 & zeta |^ 2 = (- zeta) - 1 ) by LZ23;

theorem :: FIELD_10:15

( zeta is CRoot of 3,1 & zeta ^2 is CRoot of 3,1 ) by lemCRo2;

theorem :: FIELD_10:16

3-Root(2) |^ 3 = 2 by R32;

theorem :: FIELD_10:17

X^3-1 = (X- (1. F_Rat)) * X^2+X+1 by lemX3;

theorem :: FIELD_10:18

( deg X^2-2 = 2 & deg X^3-2 = 3 & deg X^3-1 = 3 & deg X^2+X+1 = 2 ) by LL;

theorem :: FIELD_10:19

for x being Element of F_Rat holds eval (X^2-2,x) = (x |^ 2) - 2 by LKX2;

theorem :: FIELD_10:20

for x being Element of F_Rat holds eval (X^3-1,x) = (x |^ 3) - 1 by LL31;

theorem :: FIELD_10:21

for x being Element of F_Rat holds eval (X^2+X+1,x) = ((x |^ 2) + x) + 1 by LL32;

theorem :: FIELD_10:22

for x being Element of F_Rat holds eval (X^3-2,x) = (x |^ 3) - 2 by LL3;

theorem :: FIELD_10:23

for r being Element of F_Real holds Ext_eval (X^2-2,r) = (r |^ 2) - 2 by LKX2ext;

theorem :: FIELD_10:24

for z being Element of F_Complex holds Ext_eval (X^3-1,z) = (z |^ 3) - 1 by evalext1;

theorem :: FIELD_10:25

for z being Element of F_Complex holds Ext_eval (X^2+X+1,z) = ((z |^ 2) + z) + 1 by evalext11;

theorem evalext2: :: FIELD_10:26

for z being Element of F_Complex holds Ext_eval (X^3-2,z) = (z |^ 3) - 2

proof end;

theorem :: FIELD_10:27

for z being Element of the carrier of F_Complex holds
( Ext_eval (X^3-1,z) = 0. F_Complex iff z is CRoot of 3,1 ) by lemCRo;

theorem :: FIELD_10:28

Discriminant X^2+X+1 = - 3

proof end;

theorem :: FIELD_10:29

FAdj (F_Rat,{zeta}) = FAdj (F_Rat,{sqrt(-3)})

proof end;

theorem mp: :: FIELD_10:30

MinPoly (2-Root(2),F_Rat) = X^2-2

proof end;

theorem :: FIELD_10:31

deg ((FAdj (F_Rat,{2-Root(2)})),F_Rat) = 2 by LL, mp, FIELD_6:67;

theorem :: FIELD_10:32

{1,(sqrt 2)} is Basis of (VecSp ((FAdj (F_Rat,{2-Root(2)})),F_Rat))

proof end;

theorem :: FIELD_10:33

Roots X^2-2 = {} ;

theorem :: FIELD_10:34

not X^2-2 splits_in F_Rat

proof end;

theorem 2splitb: :: FIELD_10:35

Roots (F_Real,X^2-2) = {2-Root(2),(- 2-Root(2))}

proof end;

theorem 2splita: :: FIELD_10:36

X^2-2 = (X- 2-Root(2)) * (X+ 2-Root(2))

proof end;

theorem 2split: :: FIELD_10:37

FAdj (F_Rat,{2-Root(2)}) is SplittingField of X^2-2

proof end;

theorem nnn: :: FIELD_10:38

3-Root(2) is not Element of (FAdj (F_Rat,{2-Root(2)}))

proof end;

theorem :: FIELD_10:39

F_Real is not SplittingField of X^2-2

proof end;

theorem :: FIELD_10:40

F_Complex is not SplittingField of X^2-2

proof end;

theorem :: FIELD_10:41

Roots X^3-1 = {1}

proof end;

theorem :: FIELD_10:42

Roots X^2+X+1 = {} ;

theorem minpzeta: :: FIELD_10:43

MinPoly (zeta,F_Rat) = X^2+X+1

proof end;

theorem :: FIELD_10:44

Roots (F_Complex,X^3-1) = {1,zeta,(zeta ^2)} by lemroots3;

theorem :: FIELD_10:45

Roots (F_Complex,X^2+X+1) = {zeta,(zeta ^2)} by rootz;

theorem :: FIELD_10:46

not X^3-1 splits_in F_Rat

proof end;

theorem :: FIELD_10:47

not X^3-1 splits_in F_Real

proof end;

theorem :: FIELD_10:48

not X^2+X+1 splits_in F_Rat

proof end;

theorem :: FIELD_10:49

not X^2+X+1 splits_in F_Real

proof end;

theorem lemX3a: :: FIELD_10:50

X^2+X+1 = (X- zeta) * (X- (zeta ^2))

proof end;

theorem :: FIELD_10:51

X^3-1 = ((X- (1. F_Complex)) * (X- zeta)) * (X- (zeta ^2))

proof end;

theorem Xsplit: :: FIELD_10:52

FAdj (F_Rat,{zeta}) is SplittingField of X^2+X+1

proof end;

theorem Ysplit: :: FIELD_10:53

FAdj (F_Rat,{zeta}) is SplittingField of X^3-1

proof end;

theorem :: FIELD_10:54

deg ((FAdj (F_Rat,{zeta})),F_Rat) = 2 by minpzeta, LL, FIELD_6:67;

theorem baseZ: :: FIELD_10:55

{1,zeta} is Basis of (VecSp ((FAdj (F_Rat,{zeta})),F_Rat))

proof end;

theorem ns2: :: FIELD_10:56

sqrt 2 is not Element of (FAdj (F_Rat,{zeta}))

proof end;

theorem :: FIELD_10:57

F_Complex is not SplittingField of X^2+X+1

proof end;

theorem :: FIELD_10:58

F_Complex is not SplittingField of X^3-1

proof end;

theorem minpolzeta: :: FIELD_10:59

MinPoly (3-Root(2),F_Rat) = X^3-2 by LL2, FIELD_6:52;

theorem :: FIELD_10:60

deg ((FAdj (F_Rat,{3-Root(2)})),F_Rat) = 3 by LL, minpolzeta, FIELD_6:67;

theorem bas3R: :: FIELD_10:61

{1,3-Root(2),(3-Root(2) ^2)} is Basis of (VecSp ((FAdj (F_Rat,{3-Root(2)})),F_Rat))

proof end;

theorem :: FIELD_10:62

Roots X^3-2 = {}

proof end;

theorem :: FIELD_10:63

not X^3-2 splits_in F_Rat

proof end;

lemroots: Roots (F_Complex,X^3-2) = {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))}

proof end;

lemnotsplit: ( not 3-Root(2) * zeta in REAL & not 3-Root(2) * (zeta ^2) in REAL )

proof end;

theorem :: FIELD_10:64

Roots ((FAdj (F_Rat,{3-Root(2)})),X^3-2) = {3-Root(2)}

proof end;

theorem :: FIELD_10:65

not X^3-2 splits_in FAdj (F_Rat,{3-Root(2)})

proof end;

theorem :: FIELD_10:66

Roots (F_Real,X^3-2) = {3-Root(2)}

proof end;

theorem :: FIELD_10:67

not X^3-2 splits_in F_Real

proof end;

theorem :: FIELD_10:68

Roots (F_Complex,X^3-2) = {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} by lemroots;

theorem :: FIELD_10:69

X^3-2 = ((X- 3-CRoot(2)) * (X- (3-CRoot(2) * zeta))) * (X- (3-CRoot(2) * (zeta ^2)))

proof end;

theorem 32split: :: FIELD_10:70

FAdj (F_Rat,{3-CRoot(2),zeta}) is SplittingField of X^3-2

proof end;

registration

cluster F_Complex -> FAdj (F_Rat,{3-CRoot(2)}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{3-CRoot(2)}) -extending ;

cluster FieldAdjunction (F_Rat,{3-CRoot(2),zeta}) -> FAdj (F_Rat,{3-CRoot(2)}) -extending ;

coherence
FAdj (F_Rat,{3-CRoot(2),zeta}) is FAdj (F_Rat,{3-CRoot(2)}) -extending ;

end;

registration

cluster zeta -> non zero FAdj (F_Rat,{3-CRoot(2)}) -algebraic ;

coherence
zeta is FAdj (F_Rat,{3-CRoot(2)}) -algebraic

proof end;

end;

theorem mmm: :: FIELD_10:71

MinPoly (zeta,(FAdj (F_Rat,{3-CRoot(2)}))) = X^2+X+1

proof end;

theorem mml: :: FIELD_10:72

deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)}))) = 2

proof end;

theorem baszeta: :: FIELD_10:73

{1,zeta} is Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)}))))

proof end;

theorem grad6: :: FIELD_10:74

deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),F_Rat) = 6

proof end;

theorem :: FIELD_10:75

{1,3-Root(2),(3-Root(2) ^2),zeta,(3-Root(2) * zeta),((3-Root(2) ^2) * zeta)} is Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2),zeta})),F_Rat))

proof end;

registration

cluster F_Complex -> FAdj (F_Rat,{2-CRoot(2)}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{2-CRoot(2)}) -extending by FIELD_4:7;

cluster F_Complex -> FAdj (F_Rat,{2-CRoot(2),zeta}) -extending ;

coherence
F_Complex is FAdj (F_Rat,{2-CRoot(2),zeta}) -extending by FIELD_4:7;

cluster FieldAdjunction (F_Rat,{2-CRoot(2),zeta}) -> FAdj (F_Rat,{2-CRoot(2)}) -extending ;

coherence
FAdj (F_Rat,{2-CRoot(2),zeta}) is FAdj (F_Rat,{2-CRoot(2)}) -extending ;

cluster FieldAdjunction (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) -> FAdj (F_Rat,{2-CRoot(2),zeta}) -extending ;

coherence
FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) is FAdj (F_Rat,{2-CRoot(2),zeta}) -extending ;

end;

registration

cluster zeta -> non zero FAdj (F_Rat,{2-CRoot(2)}) -algebraic ;

coherence
zeta is FAdj (F_Rat,{2-CRoot(2)}) -algebraic

proof end;

cluster 3-CRoot(2) -> non zero FAdj (F_Rat,{2-CRoot(2),zeta}) -algebraic ;

coherence
3-CRoot(2) is FAdj (F_Rat,{2-CRoot(2),zeta}) -algebraic

proof end;

end;

registration

cluster FieldAdjunction (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) -> FAdj (F_Rat,{2-CRoot(2),zeta}) -finite ;

coherence
FAdj (F_Rat,{3-CRoot(2),zeta,2-CRoot(2)}) is FAdj (F_Rat,{2-CRoot(2),zeta}) -finite

proof end;

end;

theorem mmmz: :: FIELD_10:76

MinPoly (zeta,(FAdj (F_Rat,{2-CRoot(2)}))) = X^2+X+1

proof end;

theorem mmmza: :: FIELD_10:77

deg ((FAdj (F_Rat,{2-CRoot(2),zeta})),(FAdj (F_Rat,{2-CRoot(2)}))) = 2

proof end;

theorem grad4: :: FIELD_10:78

deg ((FAdj (F_Rat,{2-CRoot(2),zeta})),F_Rat) = 4

proof end;

theorem ff: :: FIELD_10:79

sqrt 2 is not Element of (FAdj (F_Rat,{3-CRoot(2),zeta}))

proof end;

theorem :: FIELD_10:80

F_Complex is not SplittingField of X^3-2

proof end;