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


begin

theorem :: GR_CY_2:1
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
proofend;

:: Some properties of Cyclic Groups
theorem Th2: :: GR_CY_2:2
for G being Group
for a being Element of G holds a in gr {a}
proofend;

theorem Th3: :: GR_CY_2:3
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}
proofend;

theorem Th4: :: GR_CY_2:4
for G being Group
for a being Element of G holds gr {a} is cyclic Group
proofend;

theorem Th5: :: GR_CY_2:5
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} )
proofend;

theorem Th6: :: GR_CY_2:6
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} )
proofend;

theorem Th7: :: GR_CY_2:7
for G being strict Group
for a being Element of G st G is finite &amp; G = gr {a} holds
for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}
proofend;

theorem Th8: :: GR_CY_2:8
for n, p, s being Element of NAT
for G being finite Group
for a being Element of G st G = gr {a} &amp; card G = n &amp; n = p * s holds
ord (a |^ p) = s
proofend;

theorem Th9: :: GR_CY_2:9
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)}
proofend;

theorem Th10: :: GR_CY_2:10
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)}) &amp; a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
proofend;

theorem Th11: :: GR_CY_2:11
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 &amp; G = gr {a} &amp; card G1 = p &amp; G1 = gr {(a |^ k)} holds
n divides k * p
proofend;

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

theorem Th13: :: GR_CY_2:13
for Gc being cyclic Group
for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} &amp; g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
proofend;

theorem Th14: :: GR_CY_2:14
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 &amp; g |^ i = g |^ i1 ) )
proofend;

registration
let n be non zero Nat;
cluster  ->  natural for Element of the carrier of (INT.Group n);
coherence
 for b1 being Element of (INT.Group n) holds b1 is natural ;
end;

:: Isomorphisms of Cyclic Groups.
theorem Th15: :: GR_CY_2:15
for Gc being finite strict cyclic Group holds INT.Group (card Gc),Gc are_isomorphic
proofend;

theorem :: GR_CY_2:16
for Gc being strict cyclic Group st Gc is infinite holds
INT.Group ,Gc are_isomorphic
proofend;

theorem Th17: :: GR_CY_2:17
for Gc, Hc being finite strict cyclic Group st card Hc = card Gc holds
Hc,Gc are_isomorphic
proofend;

theorem Th18: :: GR_CY_2:18
for p being Element of NAT
for F, G being finite strict Group st card F = p &amp; card G = p &amp; p is prime holds
F,G are_isomorphic
proofend;

theorem :: GR_CY_2:19
for F, G being finite strict Group st card F = 2 &amp; card G = 2 holds
F,G are_isomorphic by Th18, INT_2:28;

theorem :: GR_CY_2:20
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:12, INT_2:28;

theorem :: GR_CY_2:21
for G being finite strict Group st card G = 2 holds
G is cyclic Group by GR_CY_1:21, INT_2:28;

theorem :: GR_CY_2:22
for n being Element of NAT
for G being finite strict Group st G is cyclic &amp; 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 &amp; ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
proofend;

theorem :: GR_CY_2:23
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
proofend;

theorem Th24: :: GR_CY_2:24
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 &amp; ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )
proofend;

registration
let G be Group;
cluster center G ->  normal ;
coherence
 center G is normal by GROUP_5:78;
end;

theorem :: GR_CY_2:25
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 &amp; H is cyclic Group )
proofend;

theorem Th26: :: GR_CY_2:26
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
proofend;

theorem :: GR_CY_2:27
for G, F being strict Group st G,F are_isomorphic &amp; G is cyclic holds
F is cyclic
proofend;