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. grpmndd
    14. grpcld
    15. grpplusf
    16. grpplusfo
    17. resgrpplusfrn
    18. grppropd
    19. grpprop
    20. grppropstr
    21. grpss
    22. isgrpd2e
    23. isgrpd2
    24. isgrpde
    25. isgrpd
    26. isgrpi
    27. grpsgrp
    28. dfgrp2
    29. dfgrp2e
    30. isgrpix
    31. grpidcl
    32. grpbn0
    33. grplid
    34. grprid
    35. grpn0
    36. hashfingrpnn
    37. grprcan
    38. grpinveu
    39. grpid
    40. isgrpid2
    41. grpidd2
    42. grpinvfval
    43. grpinvfvalALT
    44. grpinvval
    45. grpinvfn
    46. grpinvfvi
    47. grpsubfval
    48. grpsubfvalALT
    49. grpsubval
    50. grpinvf
    51. grpinvcl
    52. grplinv
    53. grprinv
    54. grpinvid1
    55. grpinvid2
    56. isgrpinv
    57. grplrinv
    58. grpidinv2
    59. grpidinv
    60. grpinvid
    61. grplcan
    62. grpasscan1
    63. grpasscan2
    64. grpidrcan
    65. grpidlcan
    66. grpinvinv
    67. grpinvcnv
    68. grpinv11
    69. grpinvf1o
    70. grpinvnz
    71. grpinvnzcl
    72. grpsubinv
    73. grplmulf1o
    74. grpinvpropd
    75. grpidssd
    76. grpinvssd
    77. grpinvadd
    78. grpsubf
    79. grpsubcl
    80. grpsubrcan
    81. grpinvsub
    82. grpinvval2
    83. grpsubid
    84. grpsubid1
    85. grpsubeq0
    86. grpsubadd0sub
    87. grpsubadd
    88. grpsubsub
    89. grpaddsubass
    90. grppncan
    91. grpnpcan
    92. grpsubsub4
    93. grppnpcan2
    94. grpnpncan
    95. grpnpncan0
    96. grpnnncan2
    97. dfgrp3lem
    98. dfgrp3
    99. dfgrp3e
    100. grplactfval
    101. grplactval
    102. grplactcnv
    103. grplactf1o
    104. grpsubpropd
    105. grpsubpropd2
    106. grp1
    107. grp1inv
    108. prdsinvlem
    109. prdsgrpd
    110. prdsinvgd
    111. pwsgrp
    112. pwsinvg
    113. pwssub
    114. imasgrp2
    115. imasgrp
    116. imasgrpf1
    117. qusgrp2
    118. xpsgrp
    119. mhmlem
    120. mhmid
    121. mhmmnd
    122. mhmfmhm
    123. 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