:: Primitive Roots of Unity and Cyclotomic Polynomials
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

Lm1: for k being Element of NAT holds
( not k is empty iff 1 <= k )
proof end;

scheme :: UNIROOTS:sch 1
CompIndNE{ P1[ non empty Nat] } :
for k being non empty Element of NAT holds P1[k]
provided
A1: for k being non empty Element of NAT st ( for n being non empty Element of NAT st n < k holds
P1[n] ) holds
P1[k]
proof end;

theorem :: UNIROOTS:1
canceled;

theorem Th2: :: UNIROOTS:2
for f being FinSequence st 1 <= len f holds
f | (Seg 1) = <*(f . 1)*>
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)
proof end;

theorem Th3: :: UNIROOTS:3
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
proof end;

theorem Th4: :: UNIROOTS:4
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
proof end;

theorem Th5: :: UNIROOTS:5
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
proof end;

theorem :: UNIROOTS:6
canceled;

theorem :: UNIROOTS:7
for x, y being Element of F_Complex
for r1, r2 being Real st r1 = x & r2 = y holds
( r1 * r2 = x * y & r1 + r2 = x + y ) ;

theorem Th8: :: UNIROOTS:8
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
proof end;

theorem Th9: :: UNIROOTS:9
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
proof end;

theorem Th10: :: UNIROOTS:10
for n being Element of NAT holds 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n)
proof end;

theorem Th11: :: UNIROOTS:11
for n, i being Element of 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) )
proof end;

theorem Th12: :: UNIROOTS:12
for n, i being Element of 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 Th13: :: UNIROOTS:13
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 Th14: :: UNIROOTS:14
for L being non empty unital associative multMagma
for x being Element of L
for n, m being Element of NAT holds (power L) . (x,(n * m)) = (power L) . (((power L) . (x,n)),m)
proof end;

theorem Th15: :: UNIROOTS:15
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
proof end;

theorem Th16: :: UNIROOTS:16
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
proof end;

Lm3: Z3 is finite
by MOD_2:def 23;

registration
cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V169() left_unital V178() V179() V180() domRing-like doubleLoopStr ;
existence
ex b1 being Field st b1 is finite
by Lm3, MOD_2:37;
cluster non empty non degenerated non trivial finite right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital V169() left_unital V178() V179() V180() doubleLoopStr ;
existence
ex b1 being Skew-Field st b1 is finite
by Lm3, MOD_2:37;
end;

begin

definition
let R be Skew-Field;
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
ex b1 being strict Group st
( the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 )
proof end;
uniqueness
for b1, b2 being strict Group st the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 & the carrier of b2 = NonZero R & the multF of b2 = the multF of R || the carrier of b2 holds
b1 = b2
;
end;

:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :
for R being Skew-Field
for b2 being strict Group holds
( b2 = MultGroup R iff ( the carrier of b2 = NonZero R & the multF of b2 = the multF of R || the carrier of b2 ) );

theorem :: UNIROOTS:17
canceled;

theorem :: UNIROOTS:18
for R being Skew-Field holds the carrier of R = the carrier of (MultGroup R) \/ {(0. R)}
proof end;

theorem Th19: :: UNIROOTS:19
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
proof end;

theorem Th20: :: UNIROOTS:20
for R being Skew-Field holds 1_ R = 1_ (MultGroup R)
proof end;

registration
let R be finite Skew-Field;
cluster MultGroup R -> finite strict ;
correctness
coherence
MultGroup R is finite
;
proof end;
end;

theorem :: UNIROOTS:21
for R being finite Skew-Field holds card (MultGroup R) = (card R) - 1
proof end;

theorem Th22: :: UNIROOTS:22
for R being Skew-Field
for s being set st s in the carrier of (MultGroup R) holds
s in the carrier of R
proof end;

theorem :: UNIROOTS:23
for R being Skew-Field holds the carrier of (MultGroup R) c= the carrier of R
proof end;

begin

definition
let n be non empty Element of NAT ;
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 } is Subset of F_Complex
proof end;
end;

:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :
for n being non empty 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 Th24: :: UNIROOTS:24
for n being non empty 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 )
proof end;

theorem Th25: :: UNIROOTS:25
for n being non empty Element of NAT holds 1_ F_Complex in n -roots_of_1
proof end;

theorem Th26: :: UNIROOTS:26
for n being non empty Element of NAT
for x being Element of F_Complex st x in n -roots_of_1 holds
|.x.| = 1
proof end;

theorem Th27: :: UNIROOTS:27
for n being non empty 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))**] )
proof end;

theorem Th28: :: UNIROOTS:28
for n being non empty 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
proof end;

theorem Th29: :: UNIROOTS:29
for n being non empty 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;

theorem Th30: :: UNIROOTS:30
for n being non empty Element of NAT holds card (n -roots_of_1) = n
proof end;

registration
let n be non empty Element of NAT ;
cluster n -roots_of_1 -> non empty ;
correctness
coherence
not n -roots_of_1 is empty
;
by Th25;
cluster n -roots_of_1 -> finite ;
correctness
coherence
n -roots_of_1 is finite
;
proof end;
end;

theorem Th31: :: UNIROOTS:31
for n, ni being non empty Element of NAT st ni divides n holds
ni -roots_of_1 c= n -roots_of_1
proof end;

theorem Th32: :: UNIROOTS:32
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 Element of NAT holds (power (MultGroup R)) . (x,k) = (power R) . (y,k)
proof end;

theorem Th33: :: UNIROOTS:33
for n being non empty 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
proof end;

theorem Th34: :: UNIROOTS:34
for n being non empty 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)
proof end;

theorem Th35: :: UNIROOTS:35
for n being non empty Element of NAT holds n -roots_of_1 c= the carrier of (MultGroup F_Complex)
proof end;

theorem :: UNIROOTS:36
for n being non empty Element of NAT ex x being Element of (MultGroup F_Complex) st ord x = n
proof end;

theorem Th37: :: UNIROOTS:37
for n being non empty Element of NAT
for x being Element of (MultGroup F_Complex) holds
( ord x divides n iff x in n -roots_of_1 )
proof end;

theorem Th38: :: UNIROOTS:38
for n being non empty Element of NAT holds n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }
proof end;

theorem Th39: :: UNIROOTS:39
for n being non empty 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 ) )
proof end;

definition
let n be non empty Element of NAT ;
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
ex b1 being strict Group st
( the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) )
proof end;
uniqueness
for b1, b2 being strict Group st the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) & the carrier of b2 = n -roots_of_1 & the multF of b2 = the multF of F_Complex || (n -roots_of_1) holds
b1 = b2
;
end;

:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :
for n being non empty Element of NAT
for b2 being strict Group holds
( b2 = n -th_roots_of_1 iff ( the carrier of b2 = n -roots_of_1 & the multF of b2 = the multF of F_Complex || (n -roots_of_1) ) );

theorem :: UNIROOTS:40
for n being non empty Element of NAT holds n -th_roots_of_1 is Subgroup of MultGroup F_Complex
proof end;

begin

definition
let n be non empty Nat;
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)) is Polynomial of L
proof end;
end;

:: deftheorem defines unital_poly UNIROOTS:def 4 :
for n being non empty 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)%>
by POLYNOM5:def 4;

theorem :: UNIROOTS:41
canceled;

theorem Th42: :: UNIROOTS:42
for L being non empty left_unital doubleLoopStr
for n being non empty Element of NAT holds
( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )
proof end;

theorem Th43: :: UNIROOTS:43
for L being non empty left_unital doubleLoopStr
for n being non empty Nat
for i being Nat st i <> 0 & i <> n holds
(unital_poly (L,n)) . i = 0. L
proof end;

theorem Th44: :: UNIROOTS:44
for L being non empty non degenerated well-unital doubleLoopStr
for n being non empty 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 empty Element of NAT ;
cluster unital_poly (L,n) -> non-zero ;
correctness
coherence
unital_poly (L,n) is non-zero
;
proof end;
end;

theorem Th45: :: UNIROOTS:45
for n being non empty Element of NAT
for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1
proof end;

theorem Th46: :: UNIROOTS:46
for n being non empty Element of NAT holds Roots (unital_poly (F_Complex,n)) = n -roots_of_1
proof end;

theorem Th47: :: UNIROOTS:47
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 )
proof end;

theorem Th48: :: UNIROOTS:48
for n being non empty 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 )
proof end;

theorem Th49: :: UNIROOTS:49
for n being non empty Element of NAT holds BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag
proof end;

theorem Th50: :: UNIROOTS:50
for n being non empty Element of NAT holds unital_poly (F_Complex,n) = poly_with_roots (((n -roots_of_1),1) -bag)
proof end;

theorem Th51: :: UNIROOTS:51
for n being non empty Element of NAT
for i being Element of F_Complex st i is Integer holds
eval ((unital_poly (F_Complex,n)),i) is Integer
proof end;

begin

definition
let d be non empty Nat;
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 b1 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 } & b1 = poly_with_roots ((s,1) -bag) )
proof end;
uniqueness
for b1, b2 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 } & b1 = 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 } & b2 = poly_with_roots ((s,1) -bag) ) holds
b1 = b2
;
end;

:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :
for d being non empty Nat
for b2 being Polynomial of F_Complex holds
( b2 = 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 } & b2 = poly_with_roots ((s,1) -bag) ) );

theorem Th52: :: UNIROOTS:52
cyclotomic_poly 1 = <%(- (1_ F_Complex)),(1_ F_Complex)%>
proof end;

theorem Th53: :: UNIROOTS:53
for n being non empty Element of NAT
for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non empty 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 Th54: :: UNIROOTS:54
for n being non empty 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 empty 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 Th55: :: UNIROOTS:55
for d being non empty 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 )
proof end;

theorem Th56: :: UNIROOTS:56
for d being non empty Element of NAT
for z being Element of F_Complex st z is Integer holds
eval ((cyclotomic_poly d),z) is Integer
proof end;

theorem Th57: :: UNIROOTS:57
for n, ni being non empty 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 empty 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 Th58: :: UNIROOTS:58
for n, ni being non empty 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 empty 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 Th59: :: UNIROOTS:59
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 empty 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 Th60: :: UNIROOTS:60
for n being non empty 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
proof end;

theorem Th61: :: UNIROOTS:61
for n, ni being non empty 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
proof end;

theorem :: UNIROOTS:62
for n, q being non empty 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
proof end;

theorem :: UNIROOTS:63
for n, ni, q being non empty 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)
proof end;

theorem :: UNIROOTS:64
for n being non empty 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
abs i > q - 1
proof end;