:: by Broderick Arneson and Piotr Rudnicki

::

:: Received December 30, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

Lm1: for k being Element of NAT holds

( not k is zero iff 1 <= k )

proof end;

Lm2: for f being FinSequence

for n, i being Element of NAT st i <= n holds

(f | (Seg n)) | (Seg i) = f | (Seg i)

by FINSEQ_1:5, RELAT_1:74;

theorem Th2: :: UNIROOTS:2

for f being FinSequence of F_Complex

for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) holds

|.(Product f).| = Product g

for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds

|.(f /. i).| = g . i ) holds

|.(Product f).| = Product g

proof end;

theorem Th3: :: UNIROOTS:3

for s being non empty finite Subset of F_Complex

for x being Element of F_Complex

for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT

for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds

r . i = |.(x - c).| ) holds

|.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r

for x being Element of F_Complex

for r being FinSequence of REAL st len r = card s & ( for i being Element of NAT

for c being Element of F_Complex st i in dom r & c = (canFS s) . i holds

r . i = |.(x - c).| ) holds

|.(eval ((poly_with_roots ((s,1) -bag)),x)).| = Product r

proof end;

theorem Th4: :: UNIROOTS:4

for f being FinSequence of F_Complex st ( for i being Element of NAT st i in dom f holds

f . i is integer ) holds

Sum f is integer

f . i is integer ) holds

Sum f is integer

proof end;

theorem :: UNIROOTS:5

theorem Th6: :: UNIROOTS:6

for q being Real st q > 0 holds

for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds

|.([**q,0**] - r).| > q - 1

for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0**] holds

|.([**q,0**] - r).| > q - 1

proof end;

theorem Th7: :: UNIROOTS:7

for ps being non empty FinSequence of REAL

for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds

ps . i > x ) holds

Product ps > x

for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds

ps . i > x ) holds

Product ps > x

proof end;

theorem Th9: :: UNIROOTS:9

for n, i being Nat holds

( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )

( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )

proof end;

theorem Th10: :: UNIROOTS:10

for n, i being Nat holds [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] = [**(cos (((2 * PI) * (i mod n)) / n)),(sin (((2 * PI) * (i mod n)) / n))**]

proof end;

theorem Th11: :: UNIROOTS:11

for n, i, j being Element of NAT holds [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] * [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**]

proof end;

theorem Th12: :: UNIROOTS:12

for L being non empty unital associative multMagma

for x being Element of L

for n, m being Nat holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)

for x being Element of L

for n, m being Nat holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)

proof end;

theorem Th13: :: UNIROOTS:13

for n being Element of NAT

for x being Element of F_Complex st x is Integer holds

(power F_Complex) . (x,n) is Integer

for x being Element of F_Complex st x is Integer holds

(power F_Complex) . (x,n) is Integer

proof end;

theorem Th14: :: UNIROOTS:14

for F being FinSequence of F_Complex st ( for i being Element of NAT st i in dom F holds

F . i is Integer ) holds

Sum F is Integer

F . i is Integer ) holds

Sum F is Integer

proof end;

Lm3: Z_3 is finite

by MOD_2:def 20;

registration

ex b_{1} being Field st b_{1} is finite
by Lm3, MOD_2:27;

ex b_{1} being Skew-Field st b_{1} is finite
by Lm3, MOD_2:27;

end;

cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V181() left_unital V191() V192() V193() domRing-like for doubleLoopStr ;

existence ex b

cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital V181() left_unital V191() V192() V193() for doubleLoopStr ;

existence ex b

definition

let R be Skew-Field;

ex b_{1} being strict Group st

( the carrier of b_{1} = NonZero R & the multF of b_{1} = the multF of R || the carrier of b_{1} )

for b_{1}, b_{2} being strict Group st the carrier of b_{1} = NonZero R & the multF of b_{1} = the multF of R || the carrier of b_{1} & the carrier of b_{2} = NonZero R & the multF of b_{2} = the multF of R || the carrier of b_{2} holds

b_{1} = b_{2}
;

end;
func MultGroup R -> strict Group means :Def1: :: UNIROOTS:def 1

( the carrier of it = NonZero R & the multF of it = the multF of R || the carrier of it );

existence ( the carrier of it = NonZero R & the multF of it = the multF of R || the carrier of it );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :

for R being Skew-Field

for b_{2} being strict Group holds

( b_{2} = MultGroup R iff ( the carrier of b_{2} = NonZero R & the multF of b_{2} = the multF of R || the carrier of b_{2} ) );

for R being Skew-Field

for b

( b

theorem Th16: :: UNIROOTS:16

for R being Skew-Field

for a, b being Element of R

for c, d being Element of (MultGroup R) st a = c & b = d holds

c * d = a * b

for a, b being Element of R

for c, d being Element of (MultGroup R) st a = c & b = d holds

c * d = a * b

proof end;

registration
end;

theorem Th19: :: UNIROOTS:19

for R being Skew-Field

for s being set st s in the carrier of (MultGroup R) holds

s in the carrier of R

for s being set st s in the carrier of (MultGroup R) holds

s in the carrier of R

proof end;

definition

let n be non zero Element of NAT ;

{ x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } is Subset of F_Complex

end;
func n -roots_of_1 -> Subset of F_Complex equals :: UNIROOTS:def 2

{ x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;

coherence { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;

{ x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } is Subset of F_Complex

proof end;

:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :

for n being non zero Element of NAT holds n -roots_of_1 = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;

for n being non zero Element of NAT holds n -roots_of_1 = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;

theorem Th21: :: UNIROOTS:21

for n being non zero Element of NAT

for x being Element of F_Complex holds

( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex )

for x being Element of F_Complex holds

( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex )

proof end;

theorem Th23: :: UNIROOTS:23

for n being non zero Element of NAT

for x being Element of F_Complex st x in n -roots_of_1 holds

|.x.| = 1

for x being Element of F_Complex st x in n -roots_of_1 holds

|.x.| = 1

proof end;

theorem Th24: :: UNIROOTS:24

for n being non zero Element of NAT

for x being Element of F_Complex holds

( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] )

for x being Element of F_Complex holds

( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] )

proof end;

theorem Th25: :: UNIROOTS:25

for n being non zero Element of NAT

for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds

x * y in n -roots_of_1

for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds

x * y in n -roots_of_1

proof end;

theorem Th26: :: UNIROOTS:26

for n being non zero Element of NAT holds n -roots_of_1 = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n }

proof end;

registration

let n be non zero Element of NAT ;

correctness

coherence

not n -roots_of_1 is empty ;

by Th22;

correctness

coherence

n -roots_of_1 is finite ;

end;
correctness

coherence

not n -roots_of_1 is empty ;

by Th22;

correctness

coherence

n -roots_of_1 is finite ;

proof end;

theorem Th29: :: UNIROOTS:29

for R being Skew-Field

for x being Element of (MultGroup R)

for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

for x being Element of (MultGroup R)

for y being Element of R st y = x holds

for k being Nat holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)

proof end;

theorem Th30: :: UNIROOTS:30

for n being non zero Element of NAT

for x being Element of (MultGroup F_Complex) st x in n -roots_of_1 holds

not x is being_of_order_0

for x being Element of (MultGroup F_Complex) st x in n -roots_of_1 holds

not x is being_of_order_0

proof end;

theorem Th31: :: UNIROOTS:31

for n being non zero Element of NAT

for k being Element of NAT

for x being Element of (MultGroup F_Complex) st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds

ord x = n div (k gcd n)

for k being Element of NAT

for x being Element of (MultGroup F_Complex) st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds

ord x = n div (k gcd n)

proof end;

theorem Th34: :: UNIROOTS:34

for n being non zero Element of NAT

for x being Element of (MultGroup F_Complex) holds

( ord x divides n iff x in n -roots_of_1 )

for x being Element of (MultGroup F_Complex) holds

( ord x divides n iff x in n -roots_of_1 )

proof end;

theorem Th35: :: UNIROOTS:35

for n being non zero Element of NAT holds n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }

proof end;

theorem Th36: :: UNIROOTS:36

for n being non zero Element of NAT

for x being set holds

( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st

( x = y & ord y divides n ) )

for x being set holds

( x in n -roots_of_1 iff ex y being Element of (MultGroup F_Complex) st

( x = y & ord y divides n ) )

proof end;

definition

let n be non zero Element of NAT ;

ex b_{1} being strict Group st

( the carrier of b_{1} = n -roots_of_1 & the multF of b_{1} = the multF of F_Complex || (n -roots_of_1) )

for b_{1}, b_{2} being strict Group st the carrier of b_{1} = n -roots_of_1 & the multF of b_{1} = the multF of F_Complex || (n -roots_of_1) & the carrier of b_{2} = n -roots_of_1 & the multF of b_{2} = the multF of F_Complex || (n -roots_of_1) holds

b_{1} = b_{2}
;

end;
func n -th_roots_of_1 -> strict Group means :Def3: :: UNIROOTS:def 3

( the carrier of it = n -roots_of_1 & the multF of it = the multF of F_Complex || (n -roots_of_1) );

existence ( the carrier of it = n -roots_of_1 & the multF of it = the multF of F_Complex || (n -roots_of_1) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :

for n being non zero Element of NAT

for b_{2} being strict Group holds

( b_{2} = n -th_roots_of_1 iff ( the carrier of b_{2} = n -roots_of_1 & the multF of b_{2} = the multF of F_Complex || (n -roots_of_1) ) );

for n being non zero Element of NAT

for b

( b

definition

let n be non zero Nat;

let L be non empty left_unital doubleLoopStr ;

((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)) is Polynomial of L

end;
let L be non empty left_unital doubleLoopStr ;

func unital_poly (L,n) -> Polynomial of L equals :: UNIROOTS:def 4

((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L));

coherence ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L));

((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L)) is Polynomial of L

proof end;

:: deftheorem defines unital_poly UNIROOTS:def 4 :

for n being non zero Nat

for L being non empty left_unital doubleLoopStr holds unital_poly (L,n) = ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L));

for n being non zero Nat

for L being non empty left_unital doubleLoopStr holds unital_poly (L,n) = ((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L));

Lm4: unital_poly (F_Complex,1) = <%(- (1_ F_Complex)),(1_ F_Complex)%>

;

theorem Th38: :: UNIROOTS:38

for L being non empty left_unital doubleLoopStr

for n being non zero Element of NAT holds

( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )

for n being non zero Element of NAT holds

( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )

proof end;

theorem Th39: :: UNIROOTS:39

for L being non empty left_unital doubleLoopStr

for n being non zero Nat

for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

for n being non zero Nat

for i being Nat st i <> 0 & i <> n holds

(unital_poly (L,n)) . i = 0. L

proof end;

theorem Th40: :: UNIROOTS:40

for L being non empty non degenerated well-unital doubleLoopStr

for n being non zero Element of NAT holds len (unital_poly (L,n)) = n + 1

for n being non zero Element of NAT holds len (unital_poly (L,n)) = n + 1

proof end;

registration

let L be non empty non degenerated well-unital doubleLoopStr ;

let n be non zero Element of NAT ;

correctness

coherence

unital_poly (L,n) is non-zero ;

end;
let n be non zero Element of NAT ;

correctness

coherence

unital_poly (L,n) is non-zero ;

proof end;

theorem Th41: :: UNIROOTS:41

for n being non zero Element of NAT

for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1

for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1

proof end;

theorem Th43: :: UNIROOTS:43

for n being Element of NAT

for z being Element of F_Complex st z is Real holds

ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

for z being Element of F_Complex st z is Real holds

ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

proof end;

theorem Th44: :: UNIROOTS:44

for n being non zero Element of NAT

for x being Real ex y being Element of F_Complex st

( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 )

for x being Real ex y being Element of F_Complex st

( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 )

proof end;

theorem Th45: :: UNIROOTS:45

for n being non zero Element of NAT holds BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag

proof end;

theorem Th46: :: UNIROOTS:46

for n being non zero Element of NAT holds unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag)

proof end;

theorem Th47: :: UNIROOTS:47

for n being non zero Element of NAT

for i being Element of F_Complex st i is Integer holds

eval ((unital_poly (F_Complex,n)),i) is Integer

for i being Element of F_Complex st i is Integer holds

eval ((unital_poly (F_Complex,n)),i) is Integer

proof end;

definition

let d be non zero Nat;

ex b_{1} being Polynomial of F_Complex ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b_{1} = poly_with_roots ((s,1) -bag) )

for b_{1}, b_{2} being Polynomial of F_Complex st ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b_{1} = poly_with_roots ((s,1) -bag) ) & ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b_{2} = poly_with_roots ((s,1) -bag) ) holds

b_{1} = b_{2}
;

end;
func cyclotomic_poly d -> Polynomial of F_Complex means :Def5: :: UNIROOTS:def 5

ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & it = poly_with_roots ((s,1) -bag) );

existence ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & it = poly_with_roots ((s,1) -bag) );

ex b

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b

proof end;

uniqueness for b

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b

b

:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :

for d being non zero Nat

for b_{2} being Polynomial of F_Complex holds

( b_{2} = cyclotomic_poly d iff ex s being non empty finite Subset of F_Complex st

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b_{2} = poly_with_roots ((s,1) -bag) ) );

for d being non zero Nat

for b

( b

( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b

theorem Th49: :: UNIROOTS:49

for n being non zero Element of NAT

for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non zero Element of NAT st i in dom f holds

( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds

unital_poly (F_Complex,n) = Product f

for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non zero Element of NAT st i in dom f holds

( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds

unital_poly (F_Complex,n) = Product f

proof end;

theorem Th50: :: UNIROOTS:50

for n being non zero Element of NAT ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = (cyclotomic_poly n) *' p )

proof end;

theorem Th51: :: UNIROOTS:51

for d being non zero Element of NAT

for i being Element of NAT holds

( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer )

for i being Element of NAT holds

( ( (cyclotomic_poly d) . 0 = 1 or (cyclotomic_poly d) . 0 = - 1 ) & (cyclotomic_poly d) . i is integer )

proof end;

theorem Th52: :: UNIROOTS:52

for d being non zero Element of NAT

for z being Element of F_Complex st z is Integer holds

eval ((cyclotomic_poly d),z) is Integer

for z being Element of F_Complex st z is Integer holds

eval ((cyclotomic_poly d),z) is Integer

proof end;

theorem Th53: :: UNIROOTS:53

for n, ni being non zero Element of NAT

for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

Product f = poly_with_roots ((s,1) -bag)

for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

Product f = poly_with_roots ((s,1) -bag)

proof end;

theorem Th54: :: UNIROOTS:54

for n, ni being non zero Element of NAT st ni < n & ni divides n holds

ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )

ex f being FinSequence of the carrier of (Polynom-Ring F_Complex) ex p being Polynomial of F_Complex st

( p = Product f & dom f = Seg n & ( for i being non zero Element of NAT st i in Seg n holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) & unital_poly (F_Complex,n) = ((unital_poly (F_Complex,ni)) *' (cyclotomic_poly n)) *' p )

proof end;

theorem Th55: :: UNIROOTS:55

for i being Integer

for c being Element of F_Complex

for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds

( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds

eval (p,c) is integer

for c being Element of F_Complex

for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds

( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds

eval (p,c) is integer

proof end;

theorem Th56: :: UNIROOTS:56

for n being non zero Element of NAT

for j, k, q being Integer

for qc being Element of F_Complex st qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) holds

j divides k

for j, k, q being Integer

for qc being Element of F_Complex st qc = q & j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) holds

j divides k

proof end;

theorem Th57: :: UNIROOTS:57

for n, ni being non zero Element of NAT

for q being Integer st ni < n & ni divides n holds

for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

for q being Integer st ni < n & ni divides n holds

for qc being Element of F_Complex st qc = q holds

for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds

j divides k div l

proof end;

theorem :: UNIROOTS:58

for n, q being non zero Element of NAT

for qc being Element of F_Complex st qc = q holds

for j being Integer st j = eval ((cyclotomic_poly n),qc) holds

j divides (q |^ n) - 1

for qc being Element of F_Complex st qc = q holds

for j being Integer st j = eval ((cyclotomic_poly n),qc) holds

j divides (q |^ n) - 1

proof end;

theorem :: UNIROOTS:59

for n, ni, q being non zero Element of NAT st ni < n & ni divides n holds

for qc being Element of F_Complex st qc = q holds

for j being Integer st j = eval ((cyclotomic_poly n),qc) holds

j divides ((q |^ n) - 1) div ((q |^ ni) - 1)

for qc being Element of F_Complex st qc = q holds

for j being Integer st j = eval ((cyclotomic_poly n),qc) holds

j divides ((q |^ n) - 1) div ((q |^ ni) - 1)

proof end;

theorem :: UNIROOTS:60

for n being non zero Element of NAT st 1 < n holds

for q being Element of NAT st 1 < q holds

for qc being Element of F_Complex st qc = q holds

for i being Integer st i = eval ((cyclotomic_poly n),qc) holds

|.i.| > q - 1

for q being Element of NAT st 1 < q holds

for qc being Element of F_Complex st qc = q holds

for i being Integer st i = eval ((cyclotomic_poly n),qc) holds

|.i.| > q - 1

proof end;