:: Primitive Roots of Unity and Cyclotomic Polynomials
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003 Association of Mizar Users
Lm1:
for k being Element of NAT holds
( not k is empty iff 1 <= k )
theorem :: UNIROOTS:1
canceled;
theorem Th2: :: UNIROOTS:2
Lm2:
for f being FinSequence
for n, i being Element of NAT st i <= n holds
(f | (Seg n)) | (Seg i) = f | (Seg i)
theorem Th3: :: UNIROOTS:3
theorem Th4: :: UNIROOTS:4
theorem Th5: :: UNIROOTS:5
theorem :: UNIROOTS:6
canceled;
theorem :: UNIROOTS:7
theorem Th8: :: UNIROOTS:8
theorem Th9: :: UNIROOTS:9
theorem Th10: :: UNIROOTS:10
theorem Th11: :: UNIROOTS:11
theorem Th12: :: UNIROOTS:12
theorem Th13: :: UNIROOTS:13
theorem Th14: :: UNIROOTS:14
theorem Th15: :: UNIROOTS:15
theorem Th16: :: UNIROOTS:16
Lm3:
Z3 is finite
by MOD_2:def 23;
:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :
theorem :: UNIROOTS:17
canceled;
theorem :: UNIROOTS:18
theorem Th19: :: UNIROOTS:19
theorem Th20: :: UNIROOTS:20
theorem :: UNIROOTS:21
theorem Th22: :: UNIROOTS:22
theorem :: UNIROOTS:23
:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :
theorem Th24: :: UNIROOTS:24
theorem Th25: :: UNIROOTS:25
theorem Th26: :: UNIROOTS:26
theorem Th27: :: UNIROOTS:27
theorem Th28: :: UNIROOTS:28
theorem Th29: :: UNIROOTS:29
theorem Th30: :: UNIROOTS:30
theorem Th31: :: UNIROOTS:31
theorem Th32: :: UNIROOTS:32
theorem Th33: :: UNIROOTS:33
theorem Th34: :: UNIROOTS:34
theorem Th35: :: UNIROOTS:35
theorem :: UNIROOTS:36
theorem Th37: :: UNIROOTS:37
theorem Th38: :: UNIROOTS:38
theorem Th39: :: UNIROOTS:39
:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :
theorem :: UNIROOTS:40
:: deftheorem defines unital_poly UNIROOTS:def 4 :
Lm4:
unital_poly F_Complex ,1 = <%(- (1_ F_Complex )),(1_ F_Complex )%>
by POLYNOM5:def 4;
theorem :: UNIROOTS:41
canceled;
theorem Th42: :: UNIROOTS:42
theorem Th43: :: UNIROOTS:43
theorem Th44: :: UNIROOTS:44
theorem Th45: :: UNIROOTS:45
theorem Th46: :: UNIROOTS:46
theorem Th47: :: UNIROOTS:47
theorem Th48: :: UNIROOTS:48
theorem Th49: :: UNIROOTS:49
theorem Th50: :: UNIROOTS:50
theorem Th51: :: UNIROOTS:51
:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :
theorem Th52: :: UNIROOTS:52
theorem Th53: :: UNIROOTS:53
theorem Th54: :: UNIROOTS:54
theorem Th55: :: UNIROOTS:55
theorem Th56: :: UNIROOTS:56
theorem Th57: :: UNIROOTS:57
theorem Th58: :: UNIROOTS:58
theorem Th59: :: UNIROOTS:59
theorem Th60: :: UNIROOTS:60
theorem Th61: :: UNIROOTS:61
theorem :: UNIROOTS:62
theorem :: UNIROOTS:63
theorem :: UNIROOTS:64