:: Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups :: by Dariusz Surowik :: :: Received June 5, 1992 :: Copyright (c) 1992-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, GROUP_1, GROUP_2, GRAPH_1, GROUP_6, SUBSET_1, INT_1, GR_CY_1, XXREAL_0, NEWTON, CARD_1, GROUP_4, STRUCT_0, FINSET_1, RELAT_1, ARYTM_3, NAT_1, INT_2, ALGSTR_0, ARYTM_1, FINSEQ_1, FUNCT_1, TARSKI, WELLORD1, FUNCT_2, GROUP_5, PRE_TOPC, XCMPLX_0, ORDINAL1; notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2, NUMBERS, INT_1, INT_2, CARD_1, NAT_D, GROUP_2, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_3, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, FINSEQ_1, XXREAL_0; constructors BINOP_1, DOMAIN_1, REAL_1, NAT_D, BINOP_2, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, RELSET_1; registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1, MEMBERED, CARD_1; 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,m,n,p,s for Element of NAT; reserve i0,i,i1,i2 for Integer; reserve j,j1 for Element of INT.Group; reserve x,y,t for set; theorem :: GR_CY_2:1 ord a>1 & a=b|^k implies k<>0; :: Some properties of Cyclic Groups theorem :: GR_CY_2:2 a in gr {a}; theorem :: GR_CY_2:3 a=a1 implies gr {a} = gr {a1}; theorem :: GR_CY_2:4 gr {a} is cyclic Group; theorem :: GR_CY_2:5 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:6 for G being strict finite Group,b being Element of G holds (for a being Element of G holds ex p st a=b|^p) iff G = gr {b}; theorem :: GR_CY_2:7 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:8 for G being finite Group, a being Element of G holds G=gr {a} & card G = n & n = p * s implies ord (a|^p) = s; theorem :: GR_CY_2:9 s divides k implies a|^k in gr {a|^s}; theorem :: GR_CY_2:10 for G being finite Group, a being Element of G holds card gr {a |^s} = card gr {a|^k} & a|^k in gr {a|^s} implies gr {a|^s} = gr {a|^k}; theorem :: GR_CY_2:11 for G being finite Group, G1 being Subgroup of G, a being Element of G holds card G = n & G=gr {a} & card G1 = p & G1= gr{a|^k} implies n divides k*p; theorem :: GR_CY_2:12 for G being strict finite Group, a be Element of G holds G = gr {a} & card G = n implies ( G = gr {a|^k} iff k gcd n = 1 ); theorem :: GR_CY_2:13 Gc = gr {g} & g in H implies the multMagma of Gc = the multMagma of H; theorem :: GR_CY_2:14 Gc = gr {g} implies ( Gc is finite iff ex i,i1 st i<>i1 & g|^i = g|^i1 ); registration let n be non zero Nat; cluster -> natural for Element of INT.Group(n); end; :: Isomorphisms of Cyclic Groups. theorem :: GR_CY_2:15 for Gc being strict finite cyclic Group holds INT.Group(card Gc),Gc are_isomorphic; theorem :: GR_CY_2:16 for Gc being strict cyclic Group st Gc is infinite holds INT.Group,Gc are_isomorphic; theorem :: GR_CY_2:17 for Gc, Hc being strict finite cyclic Group st card Hc = card Gc holds Hc,Gc are_isomorphic; theorem :: GR_CY_2:18 for F,G being strict finite Group st card F = p & card G = p & p is prime holds F,G are_isomorphic; theorem :: GR_CY_2:19 for F,G being strict finite Group st card F = 2 & card G = 2 holds F,G are_isomorphic; theorem :: GR_CY_2:20 for G being strict finite Group holds card G = 2 implies for H being strict Subgroup of G holds H = (1).G or H = G; theorem :: GR_CY_2:21 for G being strict finite Group st card G = 2 holds G is cyclic Group; theorem :: GR_CY_2:22 for G being strict finite Group st G is cyclic & card G = n holds for p 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; theorem :: GR_CY_2:23 Gc=gr{g} implies for G,f holds g in Image f implies f is onto; theorem :: GR_CY_2:24 for Gc being strict finite cyclic Group st (ex k 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; registration let G; cluster center G -> normal; end; theorem :: GR_CY_2:25 for Gc being strict finite cyclic Group st ex k st card Gc = 2*k holds ex H being Subgroup of Gc st card H = 2 & H is cyclic Group; theorem :: GR_CY_2:26 for G being strict Group holds for g being Homomorphism of G,F st G is cyclic holds Image g is cyclic; theorem :: GR_CY_2:27 for G,F being strict Group st G,F are_isomorphic & G is cyclic holds F is cyclic;