:: Cyclic Groups and Some of Their Properties - Part I
::  by Dariusz Surowik
::
:: Received November 22, 1991
:: Copyright (c) 1991-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, 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;

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 st card G is prime holds G is cyclic;

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;