:: Algebraic Numbers
:: by Yasushige Watase
::
:: Copyright (c) 2016-2019 Association of Mizar Users

theorem Th1: :: ALGNUM_1:1
for L1, L2, L3 being Ring st L1 is Subring of L2 & L2 is Subring of L3 holds
L1 is Subring of L3
proof end;

theorem Lm1: :: ALGNUM_1:2

theorem Th3: :: ALGNUM_1:3
F_Rat is Subring of F_Complex by ;

theorem Th4: :: ALGNUM_1:4
INT.Ring is Subring of F_Complex by ;

Lm5: for A, B being Ring st A is Subring of B holds
( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B )

proof end;

Lm6: for A, B being Ring
for a being Element of A st A is Subring of B holds
a is Element of B

proof end;

Lm7:
by ;

theorem Th8: :: ALGNUM_1:5
for A, B being Ring
for x, y being Element of B
for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds
x + y = x1 + y1
proof end;

theorem Th9: :: ALGNUM_1:6
for A, B being Ring
for x, y being Element of B
for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds
x * y = x1 * y1
proof end;

registration
let c be Complex;
reduce In (c,F_Complex) to c;
reducibility
In (c,F_Complex) = c
proof end;
end;

:: Define Extended eval Function for commutative rings A c= B
:: based upon POLYNOM4
definition
let A, B be Ring;
let p be Polynomial of A;
let x be Element of B;
func Ext_eval (p,x) -> Element of B means :Def1: :: ALGNUM_1:def 1
ex F being FinSequence of B st
( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * (() . (x,(n -' 1))) ) );
existence
ex b1 being Element of B ex F being FinSequence of B st
( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * (() . (x,(n -' 1))) ) )
proof end;
uniqueness
for b1, b2 being Element of B st ex F being FinSequence of B st
( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * (() . (x,(n -' 1))) ) ) & ex F being FinSequence of B st
( b2 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * (() . (x,(n -' 1))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Ext_eval ALGNUM_1:def 1 :
for A, B being Ring
for p being Polynomial of A
for x, b5 being Element of B holds
( b5 = Ext_eval (p,x) iff ex F being FinSequence of B st
( b5 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * (() . (x,(n -' 1))) ) ) );

theorem Th11: :: ALGNUM_1:7
for n being Element of NAT
for A, B being Ring
for z being Element of A st A is Subring of B holds
() . ((In (z,B)),n) = In ((() . (z,n)),B)
proof end;

theorem Th12: :: ALGNUM_1:8
for A, B being Ring
for x1, x2 being Element of A st A is Subring of B holds
(In (x1,B)) + (In (x2,B)) = In ((x1 + x2),B)
proof end;

theorem Th13: :: ALGNUM_1:9
for A, B being Ring
for x1, x2 being Element of A st A is Subring of B holds
(In (x1,B)) * (In (x2,B)) = In ((x1 * x2),B)
proof end;

theorem Th14: :: ALGNUM_1:10
for A, B being Ring
for F being FinSequence of A
for G being FinSequence of B st A is Subring of B & F = G holds
In ((Sum F),B) = Sum G
proof end;

theorem Th15: :: ALGNUM_1:11
for A, B being Ring
for n being Nat
for x being Element of A
for p being Polynomial of A st A is Subring of B holds
(In ((p . (n -' 1)),B)) * (() . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * (() . (x,(n -' 1)))),B)
proof end;

theorem Th16: :: ALGNUM_1:12
for A, B being Ring
for x being Element of A
for p being Polynomial of A st A is Subring of B holds
Ext_eval (p,(In (x,B))) = In ((eval (p,x)),B)
proof end;

:: Modify POLYNOM4:17
theorem Th17: :: ALGNUM_1:13
for A, B being Ring
for x being Element of B holds Ext_eval ((0_. A),x) = 0. B
proof end;

:: Modify POLYNOM4:18
theorem Th18: :: ALGNUM_1:14
for A, B being non degenerated Ring
for x being Element of B st A is Subring of B holds
Ext_eval ((1_. A),x) = 1. B
proof end;

:: Modify POLYNOM4:19
theorem Th19: :: ALGNUM_1:15
for A, B being Ring
for x being Element of B
for p, q being Polynomial of A st A is Subring of B holds
Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))
proof end;

theorem Th20: :: ALGNUM_1:16
for A, B being Ring
for p, q being Polynomial of A st A is Subring of B & len p > 0 & len q > 0 holds
for x being Element of B holds Ext_eval ((),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * (() . (x,(((len p) + (len q)) -' 2)))
proof end;

theorem Th21: :: ALGNUM_1:17
for A, B being Ring
for p being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval ((),x) = (In ((p . ((len p) -' 1)),B)) * (() . (x,((len p) -' 1)))
proof end;

::Modify POLYNOM_4:Lm3:
theorem Th22: :: ALGNUM_1:18
for A being Ring
for B being comRing
for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval ((),x) = (Ext_eval ((),x)) * (Ext_eval ((),x))
proof end;

:: Modify POLYNOM4:23
theorem Th15: :: ALGNUM_1:19
for A being Ring
for B being comRing
for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval ((() *' q),x) = (Ext_eval ((),x)) * (Ext_eval (q,x))
proof end;

:: Modify POLYNOM4:24
theorem Th24: :: ALGNUM_1:20
for A being Ring
for B being comRing
for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
proof end;

:: modified POLYNOM5:37
theorem Th25: :: ALGNUM_1:21
for A, B being Ring
for x being Element of B
for z0 being Element of A st A is Subring of B holds
Ext_eval (<%z0%>,x) = In (z0,B)
proof end;

:: modified POLYNOM5:44
theorem :: ALGNUM_1:22
for A, B being Ring
for x being Element of B
for z0, z1 being Element of A st A is Subring of B holds
Ext_eval (<%z0,z1%>,x) = (In (z0,B)) + ((In (z1,B)) * x)
proof end;

:: Definition of Integral Element over A in B
definition
let A, B be Ring;
let x be Element of B;
pred x is_integral_over A means :: ALGNUM_1:def 2
ex f being Polynomial of A st
( LC f = 1. A & Ext_eval (f,x) = 0. B );
end;

:: deftheorem defines is_integral_over ALGNUM_1:def 2 :
for A, B being Ring
for x being Element of B holds
( x is_integral_over A iff ex f being Polynomial of A st
( LC f = 1. A & Ext_eval (f,x) = 0. B ) );

theorem Th27: :: ALGNUM_1:23
for B being Ring
for A being non degenerated Ring
for a being Element of A st A is Subring of B holds
In (a,B) is_integral_over A
proof end;

definition
let A be non degenerated Ring;
let B be Ring;
assume A0: A is Subring of B ;
func integral_closure (A,B) -> non empty Subset of B equals :: ALGNUM_1:def 3
{ z where z is Element of B : z is_integral_over A } ;
coherence
{ z where z is Element of B : z is_integral_over A } is non empty Subset of B
proof end;
end;

:: deftheorem defines integral_closure ALGNUM_1:def 3 :
for A being non degenerated Ring
for B being Ring st A is Subring of B holds
integral_closure (A,B) = { z where z is Element of B : z is_integral_over A } ;

definition
let c be Complex;
attr c is algebraic means :: ALGNUM_1:def 4
ex x being Element of F_Complex st
( x = c & x is_integral_over F_Rat );
end;

:: deftheorem defines algebraic ALGNUM_1:def 4 :
for c being Complex holds
( c is algebraic iff ex x being Element of F_Complex st
( x = c & x is_integral_over F_Rat ) );

definition
let x be Element of F_Complex;
redefine attr x is algebraic means :: ALGNUM_1:def 5
x is_integral_over F_Rat ;
compatibility
( x is algebraic iff x is_integral_over F_Rat )
;
end;

:: deftheorem defines algebraic ALGNUM_1:def 5 :
for x being Element of F_Complex holds
( x is algebraic iff x is_integral_over F_Rat );

definition
let c be Complex;
attr c is algebraic_integer means :: ALGNUM_1:def 6
ex x being Element of F_Complex st
( x = c & x is_integral_over INT.Ring );
end;

:: deftheorem defines algebraic_integer ALGNUM_1:def 6 :
for c being Complex holds
( c is algebraic_integer iff ex x being Element of F_Complex st
( x = c & x is_integral_over INT.Ring ) );

definition
let x be Element of F_Complex;
redefine attr x is algebraic_integer means :: ALGNUM_1:def 7
x is_integral_over INT.Ring ;
compatibility ;
end;

:: deftheorem defines algebraic_integer ALGNUM_1:def 7 :
for x being Element of F_Complex holds
( x is algebraic_integer iff x is_integral_over INT.Ring );

notation
let x be Complex;
antonym transcendental x for algebraic ;
end;

registration
coherence
for b1 being Complex st b1 is rational holds
b1 is algebraic
proof end;
end;

registration
existence
ex b1 being Complex st b1 is algebraic
by GAUSSINT:14;
existence
ex b1 being Element of F_Complex st b1 is algebraic
by Lm7;
end;

registration
coherence
for b1 being Complex st b1 is integer holds
b1 is algebraic_integer
proof end;
end;

registration
existence
ex b1 being Complex st b1 is algebraic_integer
by GAUSSINT:14;
existence
ex b1 being Element of F_Complex st b1 is algebraic_integer
by Lm7;
end;

definition
let A, B be Ring;
let x be Element of B;
func Ann_Poly (x,A) -> non empty Subset of () equals :: ALGNUM_1:def 8
{ p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;
coherence
{ p where p is Polynomial of A : Ext_eval (p,x) = 0. B } is non empty Subset of ()
proof end;
end;

:: deftheorem defines Ann_Poly ALGNUM_1:def 8 :
for A, B being Ring
for x being Element of B holds Ann_Poly (x,A) = { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;

theorem Lm30: :: ALGNUM_1:24
for A, B being Ring
for w being Element of B
for x, y being Element of () st A is Subring of B & x in Ann_Poly (w,A) & y in Ann_Poly (w,A) holds
x + y in Ann_Poly (w,A)
proof end;

theorem Th31: :: ALGNUM_1:25
for A being Ring
for B being comRing
for z being Element of B
for p, x being Element of () st A is Subring of B & x in Ann_Poly (z,A) holds
p * x in Ann_Poly (z,A)
proof end;

theorem Lm32: :: ALGNUM_1:26
for A being Ring
for B being comRing
for w being Element of B
for p, x being Element of () st A is Subring of B & x in Ann_Poly (w,A) holds
x * p in Ann_Poly (w,A)
proof end;

theorem Th33: :: ALGNUM_1:27
for A being non degenerated Ring
for B being non degenerated comRing
for w being Element of B st A is Subring of B holds
Ann_Poly (w,A) is proper Ideal of ()
proof end;

theorem Th34: :: ALGNUM_1:28
for K, L being Field
for w being Element of L st K is Subring of L holds
ex g being Element of () st {g} -Ideal = Ann_Poly (w,K)
proof end;

theorem Th35: :: ALGNUM_1:29
for K, L being Field
for z being Element of L st z is_integral_over K holds
Ann_Poly (z,K) <> {(0. ())}
proof end;

theorem Lm37: :: ALGNUM_1:30
for K being Field
for p being Element of () st p <> 0_. K holds
p is non zero Element of the carrier of ()
proof end;

theorem Th38: :: ALGNUM_1:31
for K, L being Field
for w being Element of L st K is Subring of L holds
Ann_Poly (w,K) is quasi-prime
proof end;

theorem Th39: :: ALGNUM_1:32
for K, L being Field
for w being Element of L st K is Subring of L & w is_integral_over K holds
Ann_Poly (w,K) is prime
proof end;

theorem Th40: :: ALGNUM_1:33
for K, L being Field
for z being Element of L st K is Subring of L & z is_integral_over K holds
ex f being Element of () st
( f <> 0_. K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f )
proof end;

theorem Th41: :: ALGNUM_1:34
for K, L being Field
for z being Element of L
for f, g being Element of () st z is_integral_over K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f & {g} -Ideal = Ann_Poly (z,K) & g = NormPolynomial g holds
f = g
proof end;

definition
let K, L be Field;
let z be Element of L;
assume that
A1: K is Subring of L and
A2: z is_integral_over K ;
func minimal_polynom (z,K) -> Element of the carrier of () means :Def7: :: ALGNUM_1:def 9
( it <> 0_. K & {it} -Ideal = Ann_Poly (z,K) & it = NormPolynomial it );
existence
ex b1 being Element of the carrier of () st
( b1 <> 0_. K & {b1} -Ideal = Ann_Poly (z,K) & b1 = NormPolynomial b1 )
by A1, A2, Th40;
uniqueness
for b1, b2 being Element of the carrier of () st b1 <> 0_. K & {b1} -Ideal = Ann_Poly (z,K) & b1 = NormPolynomial b1 & b2 <> 0_. K & {b2} -Ideal = Ann_Poly (z,K) & b2 = NormPolynomial b2 holds
b1 = b2
by ;
end;

:: deftheorem Def7 defines minimal_polynom ALGNUM_1:def 9 :
for K, L being Field
for z being Element of L st K is Subring of L & z is_integral_over K holds
for b4 being Element of the carrier of () holds
( b4 = minimal_polynom (z,K) iff ( b4 <> 0_. K & {b4} -Ideal = Ann_Poly (z,K) & b4 = NormPolynomial b4 ) );

definition
let K, L be Field;
let z be Element of L;
assume that
A1: K is Subring of L and
A2: z is_integral_over K ;
func deg_of_integral_element (z,K) -> Element of NAT equals :: ALGNUM_1:def 10
deg (minimal_polynom (z,K));
coherence
deg (minimal_polynom (z,K)) is Element of NAT
proof end;
end;

:: deftheorem defines deg_of_integral_element ALGNUM_1:def 10 :
for K, L being Field
for z being Element of L st K is Subring of L & z is_integral_over K holds
deg_of_integral_element (z,K) = deg (minimal_polynom (z,K));

definition
let A, B be Ring;
let x be Element of B;
func hom_Ext_eval (x,A) -> Function of (),B means :Def9: :: ALGNUM_1:def 11
for p being Polynomial of A holds it . p = Ext_eval (p,x);
existence
ex b1 being Function of (),B st
for p being Polynomial of A holds b1 . p = Ext_eval (p,x)
proof end;
uniqueness
for b1, b2 being Function of (),B st ( for p being Polynomial of A holds b1 . p = Ext_eval (p,x) ) & ( for p being Polynomial of A holds b2 . p = Ext_eval (p,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines hom_Ext_eval ALGNUM_1:def 11 :
for A, B being Ring
for x being Element of B
for b4 being Function of (),B holds
( b4 = hom_Ext_eval (x,A) iff for p being Polynomial of A holds b4 . p = Ext_eval (p,x) );

registration
let x be Element of F_Complex;
coherence
( hom_Ext_eval (x,F_Rat) is unity-preserving & hom_Ext_eval (x,F_Rat) is additive & hom_Ext_eval (x,F_Rat) is multiplicative )
proof end;
end;

theorem :: ALGNUM_1:35
for x being Element of F_Complex holds F_Complex is Polynom-Ring F_Rat -homomorphic
proof end;

theorem Lm45: :: ALGNUM_1:36
for A, B being Ring
for x being Element of B
for z being object st z in rng (hom_Ext_eval (x,A)) holds
z in B ;

definition
let x be Element of F_Complex;
func FQ x -> Subset of F_Complex equals :: ALGNUM_1:def 12
rng ();
coherence
rng () is Subset of F_Complex
;
end;

:: deftheorem defines FQ ALGNUM_1:def 12 :
for x being Element of F_Complex holds FQ x = rng ();

registration
let x be Element of F_Complex;
cluster FQ x -> non empty ;
coherence
not FQ x is empty
;
end;

theorem Lm46: :: ALGNUM_1:37
for x, z1, z2 being Element of F_Complex st z1 in FQ x & z2 in FQ x holds
z1 + z2 in FQ x
proof end;

theorem Lm47: :: ALGNUM_1:38
for x, z1, z2 being Element of F_Complex st z1 in FQ x & z2 in FQ x holds
z1 * z2 in FQ x
proof end;

theorem Lm48: :: ALGNUM_1:39
for x being Element of F_Complex
for a being Element of F_Rat holds a in FQ x
proof end;

definition
let x be Element of F_Complex;
func FQ_add x -> BinOp of (FQ x) equals :: ALGNUM_1:def 13
correctness
coherence
addcomplex || (FQ x) is BinOp of (FQ x)
;
proof end;
end;

:: deftheorem defines FQ_add ALGNUM_1:def 13 :
for x being Element of F_Complex holds FQ_add x = addcomplex || (FQ x);

definition
let x be Element of F_Complex;
func FQ_mult x -> BinOp of (FQ x) equals :: ALGNUM_1:def 14
multcomplex || (FQ x);
correctness
coherence
multcomplex || (FQ x) is BinOp of (FQ x)
;
proof end;
end;

:: deftheorem defines FQ_mult ALGNUM_1:def 14 :
for x being Element of F_Complex holds FQ_mult x = multcomplex || (FQ x);

theorem Th49: :: ALGNUM_1:40
for x being Element of F_Complex
for z, w being Element of FQ x holds () . (z,w) = z + w
proof end;

theorem Th50: :: ALGNUM_1:41
for x being Element of F_Complex
for z, w being Element of FQ x holds () . (z,w) = z * w
proof end;

theorem Lm52: :: ALGNUM_1:42
for x being Element of F_Complex holds In ((),(FQ x)) = 1. F_Complex
proof end;

theorem Lm53: :: ALGNUM_1:43
In ((- ()),F_Complex) = - ()
proof end;

definition
let x be Element of F_Complex;
func FQ_Ring x -> non empty strict doubleLoopStr equals :: ALGNUM_1:def 15
doubleLoopStr(# (FQ x),(),(),(In ((),(FQ x))),(In ((),(FQ x))) #);
coherence
doubleLoopStr(# (FQ x),(),(),(In ((),(FQ x))),(In ((),(FQ x))) #) is non empty strict doubleLoopStr
;
end;

:: deftheorem defines FQ_Ring ALGNUM_1:def 15 :
for x being Element of F_Complex holds FQ_Ring x = doubleLoopStr(# (FQ x),(),(),(In ((),(FQ x))),(In ((),(FQ x))) #);

theorem Th54: :: ALGNUM_1:44
for x being Element of F_Complex holds FQ_Ring x is Ring
proof end;

registration
let x be Element of F_Complex;
coherence by Th54;
end;

registration
let z be Element of F_Complex;
coherence
( FQ_Ring z is domRing-like & FQ_Ring z is commutative & not FQ_Ring z is degenerated )
proof end;
end;

Lm55: for x being Element of F_Complex holds the carrier of F_Rat c= the carrier of ()
by Lm48;

theorem Lm56: :: ALGNUM_1:45
for x being Element of F_Complex holds
( c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= )
proof end;

theorem Lm57: :: ALGNUM_1:46
for x being Element of F_Complex holds the addF of F_Rat = the addF of () || RAT
proof end;

theorem Lm58: :: ALGNUM_1:47
for x being Element of F_Complex holds the multF of F_Rat = the multF of () || RAT
proof end;

theorem :: ALGNUM_1:48
for x being Element of F_Complex holds F_Rat is Subring of FQ_Ring x
proof end;

theorem Th80: :: ALGNUM_1:49
for K being Field
for f, g being Element of () st f <> 0. () & {f} -Ideal is prime & not g in {f} -Ideal holds
{f,g} -Ideal = the carrier of ()
proof end;

theorem Th81: :: ALGNUM_1:50
for K being Field
for f, g being Element of () st f <> 0. () & {f} -Ideal is prime & not g in {f} -Ideal holds
{f} -Ideal ,{g} -Ideal are_co-prime
proof end;

theorem Lm62: :: ALGNUM_1:51
for x being Element of F_Complex
for a being Element of () ex g being Element of st a = () . g
proof end;

theorem Th83: :: ALGNUM_1:52
for x, a being Element of F_Complex st a <> 0. F_Complex & a in the carrier of () holds
ex g being Element of st
( not g in Ann_Poly (x,F_Rat) & a = () . g )
proof end;

theorem Th84: :: ALGNUM_1:53
for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of () holds
ex f, g being Element of st
( {f} -Ideal = Ann_Poly (x,F_Rat) & not g in Ann_Poly (x,F_Rat) & a = () . g & {f} -Ideal ,{g} -Ideal are_co-prime )
proof end;

theorem Th85: :: ALGNUM_1:54
for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of () holds
ex b being Element of F_Complex st
( b in the carrier of () & a * b = 1. F_Complex )
proof end;

theorem :: ALGNUM_1:55
for x being Element of F_Complex st x is algebraic holds
FQ_Ring x is Field
proof end;