Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

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

Back to top