Metamath Proof Explorer

Table of Contents - 10.2. Groups

1. Definition and basic properties
   1. cgrp
   2. cminusg
   3. csg
   4. df-grp
   5. df-minusg
   6. df-sbg
   7. isgrp
   8. grpmnd
   9. grpcl
   10. grpass
   11. grpinvex
   12. grpideu
   13. grpplusf
   14. grpplusfo
   15. resgrpplusfrn
   16. grppropd
   17. grpprop
   18. grppropstr
   19. grpss
   20. isgrpd2e
   21. isgrpd2
   22. isgrpde
   23. isgrpd
   24. isgrpi
   25. grpsgrp
   26. dfgrp2
   27. dfgrp2e
   28. isgrpix
   29. grpidcl
   30. grpbn0
   31. grplid
   32. grprid
   33. grpn0
   34. hashfingrpnn
   35. grprcan
   36. grpinveu
   37. grpid
   38. isgrpid2
   39. grpidd2
   40. grpinvfval
   41. grpinvfvalALT
   42. grpinvval
   43. grpinvfn
   44. grpinvfvi
   45. grpsubfval
   46. grpsubfvalALT
   47. grpsubval
   48. grpinvf
   49. grpinvcl
   50. grplinv
   51. grprinv
   52. grpinvid1
   53. grpinvid2
   54. isgrpinv
   55. grplrinv
   56. grpidinv2
   57. grpidinv
   58. grpinvid
   59. grplcan
   60. grpasscan1
   61. grpasscan2
   62. grpidrcan
   63. grpidlcan
   64. grpinvinv
   65. grpinvcnv
   66. grpinv11
   67. grpinvf1o
   68. grpinvnz
   69. grpinvnzcl
   70. grpsubinv
   71. grplmulf1o
   72. grpinvpropd
   73. grpidssd
   74. grpinvssd
   75. grpinvadd
   76. grpsubf
   77. grpsubcl
   78. grpsubrcan
   79. grpinvsub
   80. grpinvval2
   81. grpsubid
   82. grpsubid1
   83. grpsubeq0
   84. grpsubadd0sub
   85. grpsubadd
   86. grpsubsub
   87. grpaddsubass
   88. grppncan
   89. grpnpcan
   90. grpsubsub4
   91. grppnpcan2
   92. grpnpncan
   93. grpnpncan0
   94. grpnnncan2
   95. dfgrp3lem
   96. dfgrp3
   97. dfgrp3e
   98. grplactfval
   99. grplactval
   100. grplactcnv
   101. grplactf1o
   102. grpsubpropd
   103. grpsubpropd2
   104. grp1
   105. grp1inv
   106. prdsinvlem
   107. prdsgrpd
   108. prdsinvgd
   109. pwsgrp
   110. pwsinvg
   111. pwssub
   112. imasgrp2
   113. imasgrp
   114. imasgrpf1
   115. qusgrp2
   116. xpsgrp
   117. mhmlem
   118. mhmid
   119. mhmmnd
   120. mhmfmhm
   121. ghmgrp
2. Group multiple operation
   1. cmg
   2. df-mulg
   3. mulgfval
   4. mulgfvalALT
   5. mulgval
   6. mulgfn
   7. mulgfvi
   8. mulg0
   9. mulgnn
   10. mulgnngsum
   11. mulgnn0gsum
   12. mulg1
   13. mulgnnp1
   14. mulg2
   15. mulgnegnn
   16. mulgnn0p1
   17. mulgnnsubcl
   18. mulgnn0subcl
   19. mulgsubcl
   20. mulgnncl
   21. mulgnn0cl
   22. mulgcl
   23. mulgneg
   24. mulgnegneg
   25. mulgm1
   26. mulgcld
   27. mulgaddcomlem
   28. mulgaddcom
   29. mulginvcom
   30. mulginvinv
   31. mulgnn0z
   32. mulgz
   33. mulgnndir
   34. mulgnn0dir
   35. mulgdirlem
   36. mulgdir
   37. mulgp1
   38. mulgneg2
   39. mulgnnass
   40. mulgnn0ass
   41. mulgass
   42. mulgassr
   43. mulgmodid
   44. mulgsubdir
   45. mhmmulg
   46. mulgpropd
   47. submmulgcl
   48. submmulg
   49. pwsmulg
3. Subgroups and Quotient groups
   1. csubg
   2. cnsg
   3. cqg
   4. df-subg
   5. df-nsg
   6. df-eqg
   7. issubg
   8. subgss
   9. subgid
   10. subggrp
   11. subgbas
   12. subgrcl
   13. subg0
   14. subginv
   15. subg0cl
   16. subginvcl
   17. subgcl
   18. subgsubcl
   19. subgsub
   20. subgmulgcl
   21. subgmulg
   22. issubg2
   23. issubgrpd2
   24. issubgrpd
   25. issubg3
   26. issubg4
   27. grpissubg
   28. resgrpisgrp
   29. subgsubm
   30. subsubg
   31. subgint
   32. 0subg
   33. trivsubgd
   34. trivsubgsnd
   35. isnsg
   36. isnsg2
   37. nsgbi
   38. nsgsubg
   39. nsgconj
   40. isnsg3
   41. subgacs
   42. nsgacs
   43. elnmz
   44. nmzbi
   45. nmzsubg
   46. ssnmz
   47. isnsg4
   48. nmznsg
   49. 0nsg
   50. nsgid
   51. 0idnsgd
   52. trivnsgd
   53. triv1nsgd
   54. 1nsgtrivd
   55. releqg
   56. eqgfval
   57. eqgval
   58. eqger
   59. eqglact
   60. eqgid
   61. eqgen
   62. eqgcpbl
   63. qusgrp
   64. quseccl
   65. qusadd
   66. qus0
   67. qusinv
   68. qussub
   69. lagsubg2
   70. lagsubg
4. Cyclic monoids and groups
   1. cycsubmel
   2. cycsubmcl
   3. cycsubm
   4. cyccom
   5. cycsubmcom
   6. cycsubggend
   7. cycsubgcl
   8. cycsubgss
   9. cycsubg
   10. cycsubgcld
   11. cycsubg2
   12. cycsubg2cl
5. Elementary theory of group homomorphisms
   1. cghm
   2. df-ghm
   3. reldmghm
   4. isghm
   5. isghm3
   6. ghmgrp1
   7. ghmgrp2
   8. ghmf
   9. ghmlin
   10. ghmid
   11. ghminv
   12. ghmsub
   13. isghmd
   14. ghmmhm
   15. ghmmhmb
   16. ghmmulg
   17. ghmrn
   18. 0ghm
   19. idghm
   20. resghm
   21. resghm2
   22. resghm2b
   23. ghmghmrn
   24. ghmco
   25. ghmima
   26. ghmpreima
   27. ghmeql
   28. ghmnsgima
   29. ghmnsgpreima
   30. ghmker
   31. ghmeqker
   32. pwsdiagghm
   33. ghmf1
   34. ghmf1o
   35. conjghm
   36. conjsubg
   37. conjsubgen
   38. conjnmz
   39. conjnmzb
   40. conjnsg
   41. qusghm
   42. ghmpropd
6. Isomorphisms of groups
   1. cgim
   2. cgic
   3. df-gim
   4. df-gic
   5. gimfn
   6. isgim
   7. gimf1o
   8. gimghm
   9. isgim2
   10. subggim
   11. gimcnv
   12. gimco
   13. brgic
   14. brgici
   15. gicref
   16. giclcl
   17. gicrcl
   18. gicsym
   19. gictr
   20. gicer
   21. gicen
   22. gicsubgen
7. Group actions
   1. cga
   2. df-ga
   3. isga
   4. gagrp
   5. gaset
   6. gagrpid
   7. gaf
   8. gafo
   9. gaass
   10. ga0
   11. gaid
   12. subgga
   13. gass
   14. gasubg
   15. gaid2
   16. galcan
   17. gacan
   18. gapm
   19. gaorb
   20. gaorber
   21. gastacl
   22. gastacos
   23. orbstafun
   24. orbstaval
   25. orbsta
   26. orbsta2
8. Centralizers and centers
   1. ccntz
   2. ccntr
   3. df-cntz
   4. df-cntr
   5. cntrval
   6. cntzfval
   7. cntzval
   8. elcntz
   9. cntzel
   10. cntzsnval
   11. elcntzsn
   12. sscntz
   13. cntzrcl
   14. cntzssv
   15. cntzi
   16. cntrss
   17. cntri
   18. resscntz
   19. cntz2ss
   20. cntzrec
   21. cntziinsn
   22. cntzsubm
   23. cntzsubg
   24. cntzidss
   25. cntzmhm
   26. cntzmhm2
   27. cntrsubgnsg
   28. cntrnsg
9. The opposite group
   1. coppg
   2. df-oppg
   3. oppgval
   4. oppgplusfval
   5. oppgplus
   6. oppglem
   7. oppgbas
   8. oppgtset
   9. oppgtopn
   10. oppgmnd
   11. oppgmndb
   12. oppgid
   13. oppggrp
   14. oppggrpb
   15. oppginv
   16. invoppggim
   17. oppggic
   18. oppgsubm
   19. oppgsubg
   20. oppgcntz
   21. oppgcntr
   22. gsumwrev
10. Symmetric groups
    1. Definition and basic properties
    2. Cayley's theorem
    3. Permutations fixing one element
    4. Transpositions in the symmetric group
    5. The sign of a permutation
11. p-Groups and Sylow groups; Sylow's theorems
    1. cod
    2. cgex
    3. cpgp
    4. cslw
    5. df-od
    6. df-gex
    7. df-pgp
    8. df-slw
    9. odfval
    10. odfvalALT
    11. odval
    12. odlem1
    13. odcl
    14. odf
    15. odid
    16. odlem2
    17. odmodnn0
    18. mndodconglem
    19. mndodcong
    20. mndodcongi
    21. oddvdsnn0
    22. odnncl
    23. odmod
    24. oddvds
    25. oddvdsi
    26. odcong
    27. odeq
    28. odval2
    29. odcld
    30. odmulgid
    31. odmulg2
    32. odmulg
    33. odmulgeq
    34. odbezout
    35. od1
    36. odeq1
    37. odinv
    38. odf1
    39. odinf
    40. dfod2
    41. odcl2
    42. oddvds2
    43. submod
    44. subgod
    45. odsubdvds
    46. odf1o1
    47. odf1o2
    48. odhash
    49. odhash2
    50. odhash3
    51. odngen
    52. gexval
    53. gexlem1
    54. gexcl
    55. gexid
    56. gexlem2
    57. gexdvdsi
    58. gexdvds
    59. gexdvds2
    60. gexod
    61. gexcl3
    62. gexnnod
    63. gexcl2
    64. gexdvds3
    65. gex1
    66. ispgp
    67. pgpprm
    68. pgpgrp
    69. pgpfi1
    70. pgp0
    71. subgpgp
    72. sylow1lem1
    73. sylow1lem2
    74. sylow1lem3
    75. sylow1lem4
    76. sylow1lem5
    77. sylow1
    78. odcau
    79. pgpfi
    80. pgpfi2
    81. pgphash
    82. isslw
    83. slwprm
    84. slwsubg
    85. slwispgp
    86. slwpss
    87. slwpgp
    88. pgpssslw
    89. slwn0
    90. subgslw
    91. sylow2alem1
    92. sylow2alem2
    93. sylow2a
    94. sylow2blem1
    95. sylow2blem2
    96. sylow2blem3
    97. sylow2b
    98. slwhash
    99. fislw
    100. sylow2
    101. sylow3lem1
    102. sylow3lem2
    103. sylow3lem3
    104. sylow3lem4
    105. sylow3lem5
    106. sylow3lem6
    107. sylow3
12. Direct products
    1. clsm
    2. cpj1
    3. df-lsm
    4. df-pj1
    5. lsmfval
    6. lsmvalx
    7. lsmelvalx
    8. lsmelvalix
    9. oppglsm
    10. lsmssv
    11. lsmless1x
    12. lsmless2x
    13. lsmub1x
    14. lsmub2x
    15. lsmval
    16. lsmelval
    17. lsmelvali
    18. lsmelvalm
    19. lsmelvalmi
    20. lsmsubm
    21. lsmsubg
    22. lsmcom2
    23. Direct products (extension)
13. Free groups
    1. cefg
    2. cfrgp
    3. cvrgp
    4. df-efg
    5. df-frgp
    6. df-vrgp
    7. efgmval
    8. efgmf
    9. efgmnvl
    10. efgrcl
    11. efglem
    12. efgval
    13. efger
    14. efgi
    15. efgi0
    16. efgi1
    17. efgtf
    18. efgtval
    19. efgval2
    20. efgi2
    21. efgtlen
    22. efginvrel2
    23. efginvrel1
    24. efgsf
    25. efgsdm
    26. efgsval
    27. efgsdmi
    28. efgsval2
    29. efgsrel
    30. efgs1
    31. efgs1b
    32. efgsp1
    33. efgsres
    34. efgsfo
    35. efgredlema
    36. efgredlemf
    37. efgredlemg
    38. efgredleme
    39. efgredlemd
    40. efgredlemc
    41. efgredlemb
    42. efgredlem
    43. efgred
    44. efgrelexlema
    45. efgrelexlemb
    46. efgrelex
    47. efgredeu
    48. efgred2
    49. efgcpbllema
    50. efgcpbllemb
    51. efgcpbl
    52. efgcpbl2
    53. frgpval
    54. frgpcpbl
    55. frgp0
    56. frgpeccl
    57. frgpgrp
    58. frgpadd
    59. frgpinv
    60. frgpmhm
    61. vrgpfval
    62. vrgpval
    63. vrgpf
    64. vrgpinv
    65. frgpuptf
    66. frgpuptinv
    67. frgpuplem
    68. frgpupf
    69. frgpupval
    70. frgpup1
    71. frgpup2
    72. frgpup3lem
    73. frgpup3
    74. 0frgp
14. Abelian groups
    1. Definition and basic properties
    2. Cyclic groups
    3. Group sum operation
    4. Group sums over (ranges of) integers
    5. Internal direct products
    6. The Fundamental Theorem of Abelian Groups
15. Simple groups
    1. Definition and basic properties
    2. Classification of abelian simple groups