:: Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups
:: by Dariusz Surowik
::
:: Received June 5, 1992
:: Copyright (c) 1992-2011 Association of Mizar Users

begin

theorem :: GR_CY_2:1

canceled;

theorem :: GR_CY_2:2

canceled;

theorem :: GR_CY_2:3

canceled;

theorem :: GR_CY_2:4

canceled;

theorem :: GR_CY_2:5

canceled;

theorem :: GR_CY_2:6

for G being Group
for a, b being Element of G
for k being Element of NAT st ord a > 1 & a = b |^ k holds
k <> 0

proof end;

theorem :: GR_CY_2:7

canceled;

theorem Th8: :: GR_CY_2:8

for G being Group
for a being Element of G holds a in gr {a}

proof end;

theorem Th9: :: GR_CY_2:9

for G being Group
for G1 being Subgroup of G
for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}

proof end;

theorem Th10: :: GR_CY_2:10

for G being Group
for a being Element of G holds gr {a} is cyclic Group

proof end;

theorem Th11: :: GR_CY_2:11

for G being strict Group
for b being Element of G holds
( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )

proof end;

theorem Th12: :: GR_CY_2:12

for G being finite strict Group
for b being Element of G holds
( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )

proof end;

theorem Th13: :: GR_CY_2:13

for G being strict Group
for a being Element of G st G is finite & G = gr {a} holds
for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}

proof end;

theorem Th14: :: GR_CY_2:14

for n, p, s being Element of NAT
for G being finite Group
for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s

proof end;

theorem Th15: :: GR_CY_2:15

for G being Group
for a being Element of G
for s, k being Element of NAT st s divides k holds
a |^ k in gr {(a |^ s)}

proof end;

theorem Th16: :: GR_CY_2:16

for s, k being Element of NAT
for G being finite Group
for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}

proof end;

theorem Th17: :: GR_CY_2:17

for n, p, k being Element of NAT
for G being finite Group
for G1 being Subgroup of G
for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds
n divides k * p

proof end;

theorem :: GR_CY_2:18

for n, k being Element of NAT
for G being finite strict Group
for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )

proof end;

theorem Th19: :: GR_CY_2:19

for Gc being cyclic Group
for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} & g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)

proof end;

theorem Th20: :: GR_CY_2:20

for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
( Gc is finite iff ex i, i1 being Integer st
( i <> i1 & g |^ i = g |^ i1 ) )

proof end;

definition

let n be Element of NAT ;
assume A1: n > 0 ;
let h be Element of (INT.Group n);
func @ h -> Element of NAT equals :Def1: :: GR_CY_2:def 1
h;
coherence
h is Element of NAT

proof end;

end;

:: deftheorem Def1 defines @ GR_CY_2:def 1 :
for n being Element of NAT st n > 0 holds
for h being Element of (INT.Group n) holds @ h = h;

theorem Th21: :: GR_CY_2:21

for Gc being finite strict cyclic Group holds INT.Group (card Gc),Gc are_isomorphic

proof end;

theorem :: GR_CY_2:22

for Gc being strict cyclic Group st not Gc is finite holds
INT.Group ,Gc are_isomorphic

proof end;

theorem Th23: :: GR_CY_2:23

for Gc, Hc being finite strict cyclic Group st card Hc = card Gc holds
Hc,Gc are_isomorphic

proof end;

theorem Th24: :: GR_CY_2:24

for p being Element of NAT
for F, G being finite strict Group st card F = p & card G = p & p is prime holds
F,G are_isomorphic

proof end;

theorem :: GR_CY_2:25

for F, G being finite strict Group st card F = 2 & card G = 2 holds
F,G are_isomorphic by Th24, INT_2:44;

theorem :: GR_CY_2:26

for G being finite strict Group st card G = 2 holds
for H being strict Subgroup of G holds
( H = (1). G or H = G ) by GR_CY_1:32, INT_2:44;

theorem :: GR_CY_2:27

for G being finite strict Group st card G = 2 holds
G is cyclic Group by GR_CY_1:45, INT_2:44;

theorem :: GR_CY_2:28

for n being Element of NAT
for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )

proof end;

theorem :: GR_CY_2:29

for Gc being cyclic Group
for g being Element of Gc st Gc = gr {g} holds
for G being Group
for f being Homomorphism of G,Gc st g in Image f holds
f is onto

proof end;

theorem Th30: :: GR_CY_2:30

for Gc being finite strict cyclic Group st ex k being Element of NAT st card Gc = 2 * k holds
ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )

proof end;

registration

let G be Group;
cluster center G -> normal ;
coherence
center G is normal by GROUP_5:90;

end;

theorem :: GR_CY_2:31

for Gc being finite strict cyclic Group st ex k being Element of NAT st card Gc = 2 * k holds
ex H being Subgroup of Gc st
( card H = 2 & H is cyclic Group )

proof end;

theorem Th32: :: GR_CY_2:32

for F being Group
for G being strict Group
for g being Homomorphism of G,F st G is cyclic holds
Image g is cyclic

proof end;

theorem :: GR_CY_2:33

for G, F being strict Group st G,F are_isomorphic & G is cyclic holds
F is cyclic

proof end;