:: Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups
:: by Dariusz Surowik
::
:: Received June 5, 1992
:: Copyright (c) 1992-2021 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;