:: Algebraic Numbers
:: by Yasushige Watase
::
:: Received December 15, 2016
:: Copyright (c) 2016-2021 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

F_Rat is Subfield of F_Complex by EC_PF_1:5, GAUSSINT:14, RING_3:48;

theorem Th3: :: ALGNUM_1:3

F_Rat is Subring of F_Complex by RING_3:43, Lm1;

theorem Th4: :: ALGNUM_1:4

INT.Ring is Subring of F_Complex by RING_3:47, Th3, Th1;

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: ( In ((0. F_Rat),F_Complex) = 0. F_Complex & In ((1. F_Rat),F_Complex) = 1. F_Complex & In ((0. INT.Ring),F_Complex) = 0. F_Complex & In ((1. INT.Ring),F_Complex) = 1. F_Complex )
by Lm5, Th3, Th4;

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)) * ((power B) . (x,(n -' 1))) ) );

existence
ex b₁ being Element of B ex F being FinSequence of B st
( b₁ = 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)) * ((power B) . (x,(n -' 1))) ) )

proof end;

uniqueness
for b₁, b₂ being Element of B st ex F being FinSequence of B st
( b₁ = 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)) * ((power B) . (x,(n -' 1))) ) ) & ex F being FinSequence of B st
( b₂ = 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)) * ((power B) . (x,(n -' 1))) ) ) holds
b₁ = b₂

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, b₅ being Element of B holds
( b₅ = Ext_eval (p,x) iff ex F being FinSequence of B st
( b₅ = 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)) * ((power 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
(power B) . ((In (z,B)),n) = In (((power A) . (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)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (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 (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power 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 ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power 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 (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),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 (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),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
( x is algebraic_integer iff x is_integral_over INT.Ring ) ;

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

cluster complex rational -> algebraic for object ;

coherence
for b₁ being Complex st b₁ is rational holds
b₁ is algebraic

proof end;

end;

registration

cluster complex algebraic for object ;

existence
ex b₁ being Complex st b₁ is algebraic by GAUSSINT:14;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable complex reducible algebraic for Element of the carrier of F_Complex;

existence
ex b₁ being Element of F_Complex st b₁ is algebraic by Lm7;

end;

registration

cluster integer complex -> algebraic_integer for object ;

coherence
for b₁ being Complex st b₁ is integer holds
b₁ is algebraic_integer

proof end;

end;

registration

cluster complex algebraic_integer for object ;

existence
ex b₁ being Complex st b₁ is algebraic_integer by GAUSSINT:14;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable complex reducible algebraic_integer for Element of the carrier of F_Complex;

existence
ex b₁ being Element of F_Complex st b₁ 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 (Polynom-Ring A) 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 (Polynom-Ring A)

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 (Polynom-Ring A) 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 (Polynom-Ring A) 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 (Polynom-Ring A) 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 (Polynom-Ring A)

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 (Polynom-Ring K) 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. (Polynom-Ring K))}

proof end;

theorem Lm37: :: ALGNUM_1:30

for K being Field
for p being Element of (Polynom-Ring K) st p <> 0_. K holds
p is non zero Element of the carrier of (Polynom-Ring K)

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 (Polynom-Ring K) 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 (Polynom-Ring K) 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 (Polynom-Ring K) means :Def7: :: ALGNUM_1:def 9
( it <> 0_. K & {it} -Ideal = Ann_Poly (z,K) & it = NormPolynomial it );

existence
ex b₁ being Element of the carrier of (Polynom-Ring K) st
( b₁ <> 0_. K & {b₁} -Ideal = Ann_Poly (z,K) & b₁ = NormPolynomial b₁ ) by A1, A2, Th40;
uniqueness
for b₁, b₂ being Element of the carrier of (Polynom-Ring K) st b₁ <> 0_. K & {b₁} -Ideal = Ann_Poly (z,K) & b₁ = NormPolynomial b₁ & b₂ <> 0_. K & {b₂} -Ideal = Ann_Poly (z,K) & b₂ = NormPolynomial b₂ holds
b₁ = b₂ by Th41, A2;

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 b₄ being Element of the carrier of (Polynom-Ring K) holds
( b₄ = minimal_polynom (z,K) iff ( b₄ <> 0_. K & {b₄} -Ideal = Ann_Poly (z,K) & b₄ = NormPolynomial b₄ ) );

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 (Polynom-Ring A),B means :Def9: :: ALGNUM_1:def 11
for p being Polynomial of A holds it . p = Ext_eval (p,x);

existence
ex b₁ being Function of (Polynom-Ring A),B st
for p being Polynomial of A holds b₁ . p = Ext_eval (p,x)

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring A),B st ( for p being Polynomial of A holds b₁ . p = Ext_eval (p,x) ) & ( for p being Polynomial of A holds b₂ . p = Ext_eval (p,x) ) holds
b₁ = b₂

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 b₄ being Function of (Polynom-Ring A),B holds
( b₄ = hom_Ext_eval (x,A) iff for p being Polynomial of A holds b₄ . p = Ext_eval (p,x) );

registration

let x be Element of F_Complex;

cluster hom_Ext_eval (x,F_Rat) -> additive unity-preserving multiplicative ;

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 (hom_Ext_eval (x,F_Rat));

coherence
rng (hom_Ext_eval (x,F_Rat)) is Subset of F_Complex ;

end;

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

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
addcomplex || (FQ x);

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 (FQ_add x) . (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 (FQ_mult x) . (z,w) = z * w

proof end;

theorem Lm52: :: ALGNUM_1:42

for x being Element of F_Complex holds In ((1. F_Complex),(FQ x)) = 1. F_Complex

proof end;

theorem Lm53: :: ALGNUM_1:43

In ((- (1. F_Rat)),F_Complex) = - (1. 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),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #);

coherence
doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(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),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(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;

cluster FQ_Ring x -> non empty right_complementable strict Abelian add-associative right_zeroed well-unital distributive associative ;

coherence
( FQ_Ring x is Abelian & FQ_Ring x is add-associative & FQ_Ring x is right_zeroed & FQ_Ring x is right_complementable & FQ_Ring x is associative & FQ_Ring x is well-unital & FQ_Ring x is distributive ) by Th54;

end;

registration

let z be Element of F_Complex;

cluster FQ_Ring z -> non empty non degenerated strict commutative domRing-like ;

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 (FQ_Ring x)
by Lm48;

theorem Lm56: :: ALGNUM_1:45

for x being Element of F_Complex holds
( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] )

proof end;

theorem Lm57: :: ALGNUM_1:46

for x being Element of F_Complex holds the addF of F_Rat = the addF of (FQ_Ring x) || RAT

proof end;

theorem Lm58: :: ALGNUM_1:47

for x being Element of F_Complex holds the multF of F_Rat = the multF of (FQ_Ring x) || 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 (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds
{f,g} -Ideal = the carrier of (Polynom-Ring K)

proof end;

theorem Th81: :: ALGNUM_1:50

for K being Field
for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {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 (FQ_Ring x) ex g being Element of (Polynom-Ring F_Rat) st a = (hom_Ext_eval (x,F_Rat)) . 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 (FQ_Ring x) holds
ex g being Element of (Polynom-Ring F_Rat) st
( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . 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 (FQ_Ring x) holds
ex f, g being Element of (Polynom-Ring F_Rat) st
( {f} -Ideal = Ann_Poly (x,F_Rat) & not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . 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 (FQ_Ring x) holds
ex b being Element of F_Complex st
( b in the carrier of (FQ_Ring x) & 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;