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

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

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

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

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

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

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

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

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

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 )

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

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

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
end;

:: Isomorphisms of Cyclic Groups.

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

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

theorem :: GR_CY_2:20

theorem :: GR_CY_2:21

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

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

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

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

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

for G being strict Group

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

Image g is cyclic

proof end;