begin
Lm1:
for k being Element of NAT holds
( not k is empty iff 1 <= k )
theorem
canceled;
theorem Th2:
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:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem
for
x,
y being
Element of
for
r1,
r2 being
Real st
r1 = x &
r2 = y holds
(
r1 * r2 = x * y &
r1 + r2 = x + y ) ;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
Lm3:
Z3 is finite
by MOD_2:def 23;
begin
:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :
theorem
canceled;
theorem
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
begin
:: deftheorem defines -roots_of_1 UNIROOTS:def 2 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem Th39:
:: deftheorem Def3 defines -th_roots_of_1 UNIROOTS:def 3 :
theorem
begin
:: deftheorem defines unital_poly UNIROOTS:def 4 :
Lm4:
unital_poly F_Complex ,1 = <%(- (1_ F_Complex )),(1_ F_Complex )%>
by POLYNOM5:def 4;
theorem
canceled;
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
begin
:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
theorem