:: Cyclic Groups and Some of Their Properties - Part I
:: by Dariusz Surowik
::
:: Received November 22, 1991
:: Copyright (c) 1991-2019 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, SUBSET_1, INT_1, GROUP_1, FINSEQ_1, XCMPLX_0, CARD_1,
XBOOLE_0, BINOP_2, FUNCT_1, BINOP_1, ARYTM_3, CARD_3, SETWISEO, RELAT_1,
TARSKI, NAT_1, SETWOP_2, FINSEQ_2, NEWTON, STRUCT_0, ORDINAL4, QC_LANG1,
GROUP_4, ARYTM_1, FINSET_1, XXREAL_0, GROUP_2, ALGSTR_0, ZFMISC_1,
REALSET1, REAL_1, INT_2, RLSUB_1, GRAPH_1, GR_CY_1, MEMBERED, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, FINSET_1, BINOP_1,
DOMAIN_1, INT_1, FINSEQ_1, FINSEQ_2, SETWISEO, SETWOP_2, BINOP_2,
REALSET1, INT_2, NAT_1, NAT_D, MEMBERED, RVSUM_1, XXREAL_0, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_4;
constructors WELLORD2, BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D,
BINOP_2, FINSOP_1, SETWOP_2, RVSUM_1, REALSET1, GROUP_4, FUNCOP_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, GROUP_2,
VALUED_0, ALGSTR_0, CARD_1, FINSEQ_2, ZFMISC_1, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve i1 for Element of INT;
reserve j1,j2,j3 for Integer;
reserve p,s,k,n for Nat;
reserve x,y,xp,yp for set;
reserve G for Group;
reserve a,b for Element of G;
reserve F for FinSequence of G;
reserve I for FinSequence of INT;
definition
redefine func addint means
:: GR_CY_1:def 1
for i1,i2 being Element of INT holds it.(i1,i2) = addreal.(i1,i2);
end;
theorem :: GR_CY_1:1
for i1 st i1 = 0 holds i1 is_a_unity_wrt addint;
theorem :: GR_CY_1:2
Sum I = addint $$ I;
definition
let I;
redefine func Sum(I) -> Element of INT equals
:: GR_CY_1:def 2
addint $$ I;
end;
theorem :: GR_CY_1:3
Sum (<*> INT) = 0;
theorem :: GR_CY_1:4
for I being FinSequence of INT holds Product(((len I)|->a)|^I) = a|^Sum I;
:: Finite groups and their some properties
theorem :: GR_CY_1:5
b in gr {a} iff ex j1 st b=a|^j1;
theorem :: GR_CY_1:6
for G being finite Group, a being Element of G holds a is not
being_of_order_0;
theorem :: GR_CY_1:7
for G being finite Group, a being Element of G holds ord a = card gr {a};
theorem :: GR_CY_1:8
for G being finite Group, a being Element of G holds ord a divides card G;
theorem :: GR_CY_1:9
for G being finite Group, a being Element of G holds a|^card G = 1_G;
theorem :: GR_CY_1:10
for G being finite Group, a being Element of G holds (a|^n)" = a
|^(card G - (n mod card G));
registration
let G be associative non empty multMagma;
cluster the multMagma of G -> associative;
end;
registration
let G be Group;
cluster the multMagma of G -> Group-like;
end;
theorem :: GR_CY_1:11
for G being strict finite Group st card G > 1 ex a being Element
of G st a <> 1_G;
theorem :: GR_CY_1:12
for G being strict finite Group st card G = p & p is prime holds for H
being strict Subgroup of G holds H = (1).G or H = G;
definition
func INT.Group -> non empty strict multMagma equals
:: GR_CY_1:def 3
multMagma(#INT,addint#);
end;
registration
cluster INT.Group -> associative Group-like;
end;
registration
cluster the carrier of INT.Group -> integer-membered;
end;
registration
let a,b be Element of INT.Group;
identify a*b with a+b;
end;
registration
let n be natural Number;
cluster Segm n -> natural-membered;
end;
definition
let n be natural Number such that
n > 0;
func addint(n) -> BinOp of Segm(n) means
:: GR_CY_1:def 4
for k,l being Element of Segm(n) holds it.(k,l) = (k+l) mod n;
end;
definition
let n be non zero Nat;
func INT.Group(n) -> non empty strict multMagma equals
:: GR_CY_1:def 5
multMagma(#Segm(n),addint(n)#);
end;
registration
let n be non zero Nat;
cluster INT.Group(n) -> finite associative Group-like;
end;
theorem :: GR_CY_1:13
1_INT.Group = 0;
theorem :: GR_CY_1:14
for n be non zero Nat holds 1_INT.Group(n) = 0;
definition
let h be Integer;
func @'h -> Element of INT.Group equals
:: GR_CY_1:def 6
h;
end;
theorem :: GR_CY_1:15
for h being Element of INT.Group holds h" = -h;
reserve G1 for Subgroup of INT.Group;
theorem :: GR_CY_1:16
j1 = (@'1) |^ j1;
definition
let IT be Group;
attr IT is cyclic means
:: GR_CY_1:def 7
ex a being Element of IT st the multMagma of IT = gr {a};
end;
registration
cluster strict cyclic for Group;
end;
registration
let G be Group;
cluster (1).G -> cyclic;
end;
registration
cluster strict finite cyclic for Group;
end;
theorem :: GR_CY_1:17
G is cyclic Group iff ex a being Element of G st for b being
Element of G ex j1 st b=a|^j1;
theorem :: GR_CY_1:18
for G being finite Group holds G is cyclic iff ex a being
Element of G st for b being Element of G ex n st b = a|^n;
theorem :: GR_CY_1:19
for G being finite Group holds ( G is cyclic iff ex a being
Element of G st ord a = card G );
theorem :: GR_CY_1:20
for G being finite Group, H being strict Subgroup of G st G is cyclic
holds H is cyclic;
theorem :: GR_CY_1:21
for G being strict finite Group holds card G is prime implies
G is cyclic Group;
theorem :: GR_CY_1:22
for n being non zero Nat
ex g being Element of INT.Group(n) st for b being
Element of INT.Group(n) ex j1 st b = g|^j1;
registration
cluster cyclic -> commutative for Group;
end;
theorem :: GR_CY_1:23
INT.Group = gr {@'1};
registration
cluster INT.Group -> cyclic;
end;
registration
let n be non zero Nat;
cluster INT.Group(n) -> cyclic;
end;