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

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

proof end;

:: 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}

proof end;

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}

proof end;

theorem Th4: :: GR_CY_2:4

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

proof end;

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} )

proof end;

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} )

proof end;

theorem Th7: :: GR_CY_2:7

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 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} & card G = n & n = p * s holds
ord (a |^ p) = s

proof end;

theorem Th9: :: GR_CY_2:9

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

proof end;

theorem Th10: :: GR_CY_2:10

for k, s 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 Th11: :: GR_CY_2:11

for k, n, p 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:12

for k, n 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 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} & 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 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 & g |^ i = g |^ i1 ) )

proof end;

registration

let n be non zero Nat;

cluster -> natural for Element of the carrier of (INT.Group n);

coherence
for b₁ being Element of (INT.Group n) holds b₁ 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

proof end;

theorem :: GR_CY_2:16

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

proof end;

theorem Th17: :: GR_CY_2:17

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

proof end;

theorem Th18: :: GR_CY_2:18

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:19

for F, G being finite strict Group st card F = 2 & 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 & 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: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

proof end;

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 & ( 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: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 & H is cyclic Group )

proof end;

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

proof end;

theorem :: GR_CY_2:27

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

proof end;