The abstract of the Mizar article:

Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups

by

Dariusz Surowik

Received June 5, 1992

MML identifier: GR_CY_2

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, GROUP_2, GRAPH_1, GROUP_6, INT_1, GR_CY_1, NAT_1,
      ARYTM_1, ARYTM_3, ABSVALUE, GROUP_1, FINSET_1, GROUP_4, VECTSP_1,
      RELAT_1, FINSEQ_1, FUNCT_1, QC_LANG1, WELLORD1, FILTER_0, GROUP_5,
      GROUP_3;
 notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, INT_1, INT_2, NAT_1, RLVECT_1, GROUP_1, GROUP_2, STRUCT_0,
      VECTSP_1, GROUP_3, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, FINSEQ_1;
 constructors REAL_1, BINOP_1, NAT_1, GROUP_4, GROUP_5, GROUP_6, GR_CY_1,
      NAT_LAT, MEMBERED, XBOOLE_0;
 clusters INT_1, GR_CY_1, STRUCT_0, XREAL_0, GROUP_2, FINSEQ_1, RELSET_1,
      GROUP_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve F,G for Group;
 reserve G1 for Subgroup of G;
 reserve Gc for cyclic Group;
 reserve H for Subgroup of Gc;
 reserve f for Homomorphism of G,Gc;
 reserve a,b for Element of G;
 reserve g for Element of Gc;
 reserve a1 for Element of G1;
 reserve k,l,m,n,p,s,r for Nat;
 reserve i0,i,i1,i2,i3,i4 for Integer;
 reserve j,j1 for Element of INT.Group;
 reserve x,y,t for set;

::::::::::::: Some properties of natural and integer numbers.:::::::::::

theorem :: GR_CY_2:1
 for n,m st 0 < m holds n mod m= n - m * (n div m);

theorem :: GR_CY_2:2
 i2 >= 0 implies i1 mod i2 >= 0;

theorem :: GR_CY_2:3
 i2 > 0 implies i1 mod i2 < i2;

theorem :: GR_CY_2:4
 i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2);

theorem :: GR_CY_2:5
 for m,n st m>0 or n>0 holds ex i,i1 st i*m + i1*n = m hcf n;

theorem :: GR_CY_2:6
   ord a>1 & a=b|^k implies k<>0;

theorem :: GR_CY_2:7
 G is finite implies ord G > 0;

:::::::::::::::::::: Some properties of Cyclic Groups ::::::::::::::::::::::

theorem :: GR_CY_2:8
 a in gr {a};

theorem :: GR_CY_2:9
 a=a1 implies gr {a} = gr {a1};

theorem :: GR_CY_2:10
 gr {a} is cyclic Group;

theorem :: GR_CY_2:11
 for G being strict Group,b being Element of G holds
  ( for a being Element of G holds ex i st a=b|^i )
    iff G= gr {b};

theorem :: GR_CY_2:12
 for G being strict Group,b being Element of G
  holds G is finite implies
  ((for a being Element of G holds ex p st a=b|^p)
   iff G = gr {b});

theorem :: GR_CY_2:13
 for G being strict Group,a being Element of G holds
  G is finite & G = gr {a} implies for G1 being strict Subgroup of G holds
   ex p st G1 = gr {a|^p};

theorem :: GR_CY_2:14
 G is finite & G=gr {a} & ord G = n & n = p * s implies ord (a|^p) = s;

theorem :: GR_CY_2:15
 s divides k implies a|^k in gr {a|^s};

theorem :: GR_CY_2:16
 G is finite & ord gr {a|^s} = ord gr {a|^k} & a|^k in gr {a|^s} implies
  gr {a|^s} = gr {a|^k};

theorem :: GR_CY_2:17
 G is finite & ord G = n & G=gr {a} & ord G1 = p & G1= gr{a|^k} implies n
 divides k*p;

theorem :: GR_CY_2:18
   for G being strict Group, a be Element of G holds
  G is finite & G = gr {a} & ord G = n implies
  ( G = gr {a|^k} iff k hcf n = 1);

theorem :: GR_CY_2:19
 Gc = gr {g} & g in H implies the HGrStr of Gc = the HGrStr of H;

theorem :: GR_CY_2:20
 Gc = gr {g} implies
  ( Gc is finite iff ex i,i1 st i<>i1 & g|^i = g|^i1 );

definition
 let n such that n>0;
 let h be Element of INT.Group(n);
 func @h -> Nat equals
:: GR_CY_2:def 1
  h;
end;

:::::::::::::::::::: Isomorphisms of Cyclic Groups. :::::::::::::::::::::::::::

theorem :: GR_CY_2:21
 for Gc being strict cyclic Group holds
  Gc is finite & ord Gc = n implies INT.Group(n),Gc are_isomorphic;

theorem :: GR_CY_2:22
   for Gc being strict cyclic Group holds
  Gc is infinite implies INT.Group,Gc are_isomorphic;

theorem :: GR_CY_2:23
 for Gc, Hc being strict cyclic Group holds
  Hc is finite & Gc is finite & ord Hc = ord Gc implies Hc,Gc are_isomorphic;

theorem :: GR_CY_2:24
 for F,G being strict Group holds
  F is finite & G is finite & ord F = p & ord G = p & p is prime implies
   F,G are_isomorphic;

theorem :: GR_CY_2:25
   for F,G being strict Group holds
  F is finite & G is finite & ord F = 2 & ord G = 2 implies
   F,G are_isomorphic;

theorem :: GR_CY_2:26
   for G being strict Group holds
  G is finite & ord G = 2 implies
   for H being strict Subgroup of G holds
    H = (1).G or H = G;

theorem :: GR_CY_2:27
   for G being strict Group holds
  G is finite & ord G = 2 implies G is cyclic Group;

theorem :: GR_CY_2:28
   for G being strict Group holds G is finite & G is cyclic Group & ord G = n
  implies (for p st p divides n holds
   (ex G1 being strict Subgroup of G st ord G1 = p &
    for G2  being strict Subgroup of G st ord G2=p holds G2=G1));

theorem :: GR_CY_2:29
   Gc=gr{g} implies (for G,f holds g in Image f implies f is_epimorphism);

theorem :: GR_CY_2:30
 for Gc being strict cyclic Group holds
  (Gc is finite & ord Gc=n & ex k st n=2*k) implies
   ex g1 being Element of Gc st ord g1 = 2 &
    for g2 being Element of Gc st ord g2=2 holds g1=g2;

definition let G;
 cluster center G -> normal;
end;

theorem :: GR_CY_2:31
   for Gc being strict cyclic Group holds
  (Gc is finite & ord Gc=n & ex k st n=2*k) implies
   ex H being Subgroup of Gc st ord H = 2 & H is cyclic Group;

theorem :: GR_CY_2:32
 for G being strict Group holds
  for g being Homomorphism of G,F holds
    G is cyclic Group implies Image g is cyclic Group;

theorem :: GR_CY_2:33
   for G,F being strict Group holds
  G,F are_isomorphic & (G is cyclic Group or F is cyclic Group) implies
   (G is cyclic Group & F is cyclic Group);