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