:: Cyclic Groups and Some of Their Properties - Part I
:: by Dariusz Surowik
::
:: Received November 22, 1991
:: Copyright (c) 1991 Association of Mizar Users
Lm1:
for x being set
for n being Element of NAT st n > 0 & x in Segm n holds
x is Element of NAT
;
theorem :: GR_CY_1:1
canceled;
theorem :: GR_CY_1:2
canceled;
theorem :: GR_CY_1:3
canceled;
theorem :: GR_CY_1:4
canceled;
theorem :: GR_CY_1:5
canceled;
theorem :: GR_CY_1:6
canceled;
theorem :: GR_CY_1:7
canceled;
theorem :: GR_CY_1:8
canceled;
theorem :: GR_CY_1:9
canceled;
theorem :: GR_CY_1:10
theorem :: GR_CY_1:11
canceled;
theorem :: GR_CY_1:12
theorem :: GR_CY_1:13
:: deftheorem GR_CY_1:def 1 :
canceled;
:: deftheorem defines addint GR_CY_1:def 2 :
theorem Th14: :: GR_CY_1:14
theorem :: GR_CY_1:15
theorem Th16: :: GR_CY_1:16
:: deftheorem defines Sum GR_CY_1:def 3 :
theorem :: GR_CY_1:17
canceled;
theorem :: GR_CY_1:18
canceled;
theorem :: GR_CY_1:19
canceled;
theorem :: GR_CY_1:20
theorem :: GR_CY_1:21
canceled;
theorem Th22: :: GR_CY_1:22
Lm2:
for G being Group
for a being Element of G holds Product (((len (<*> INT )) |-> a) |^ (<*> INT )) = a |^ (Sum (<*> INT ))
Lm3:
for G being Group
for a being Element of G
for I being FinSequence of INT
for w being Element of INT st Product (((len I) |-> a) |^ I) = a |^ (Sum I) holds
Product (((len (I ^ <*w*>)) |-> a) |^ (I ^ <*w*>)) = a |^ (Sum (I ^ <*w*>))
theorem :: GR_CY_1:23
canceled;
theorem Th24: :: GR_CY_1:24
theorem Th25: :: GR_CY_1:25
theorem Th26: :: GR_CY_1:26
theorem Th27: :: GR_CY_1:27
theorem Th28: :: GR_CY_1:28
theorem Th29: :: GR_CY_1:29
theorem Th30: :: GR_CY_1:30
theorem Th31: :: GR_CY_1:31
theorem :: GR_CY_1:32
theorem Th33: :: GR_CY_1:33
:: deftheorem defines INT.Group GR_CY_1:def 4 :
:: deftheorem Def5 defines addint GR_CY_1:def 5 :
theorem Th34: :: GR_CY_1:34
:: deftheorem Def6 defines INT.Group GR_CY_1:def 6 :
theorem Th35: :: GR_CY_1:35
theorem Th36: :: GR_CY_1:36
:: deftheorem GR_CY_1:def 7 :
canceled;
:: deftheorem defines @' GR_CY_1:def 8 :
theorem Th37: :: GR_CY_1:37
theorem Th38: :: GR_CY_1:38
theorem Th39: :: GR_CY_1:39
Lm4:
INT.Group = gr {(@' 1)}
:: deftheorem Def9 defines cyclic GR_CY_1:def 9 :
theorem Th40: :: GR_CY_1:40
theorem Th41: :: GR_CY_1:41
theorem Th42: :: GR_CY_1:42
theorem Th43: :: GR_CY_1:43
theorem :: GR_CY_1:44
theorem :: GR_CY_1:45
theorem Th46: :: GR_CY_1:46
theorem :: GR_CY_1:47
theorem Th48: :: GR_CY_1:48
theorem :: GR_CY_1:49
theorem :: GR_CY_1:50