Metamath Proof Explorer

Table of Contents - 10.2.10. Symmetric groups

1. Definition and basic properties
   1. csymg
   2. df-symg
   3. symgval
   4. symgbas
   5. elsymgbas2
   6. elsymgbas
   7. symgbasf1o
   8. symgbasf
   9. symgbasmap
   10. symghash
   11. symgbasfi
   12. symgfv
   13. symgfvne
   14. symgressbas
   15. symgplusg
   16. symgov
   17. symgcl
   18. idresperm
   19. symgmov1
   20. symgmov2
   21. symgbas0
   22. symg1hash
   23. symg1bas
   24. symg2hash
   25. symg2bas
   26. 0symgefmndeq
   27. snsymgefmndeq
   28. symgpssefmnd
   29. symgvalstruct
   30. symgsubmefmnd
   31. symgtset
   32. symggrp
   33. symgid
   34. symginv
   35. symgsubmefmndALT
   36. galactghm
   37. lactghmga
   38. symgtopn
   39. symgga
   40. pgrpsubgsymgbi
   41. pgrpsubgsymg
   42. idressubgsymg
   43. idrespermg
2. Cayley's theorem
   1. cayleylem1
   2. cayleylem2
   3. cayley
   4. cayleyth
3. Permutations fixing one element
   1. symgfix2
   2. symgextf
   3. symgextfv
   4. symgextfve
   5. symgextf1lem
   6. symgextf1
   7. symgextfo
   8. symgextf1o
   9. symgextsymg
   10. symgextres
   11. gsumccatsymgsn
   12. gsmsymgrfixlem1
   13. gsmsymgrfix
   14. fvcosymgeq
   15. gsmsymgreqlem1
   16. gsmsymgreqlem2
   17. gsmsymgreq
   18. symgfixelq
   19. symgfixels
   20. symgfixelsi
   21. symgfixf
   22. symgfixf1
   23. symgfixfolem1
   24. symgfixfo
   25. symgfixf1o
4. Transpositions in the symmetric group
   1. cpmtr
   2. df-pmtr
   3. f1omvdmvd
   4. f1omvdcnv
   5. mvdco
   6. f1omvdconj
   7. f1otrspeq
   8. f1omvdco2
   9. f1omvdco3
   10. pmtrfval
   11. pmtrval
   12. pmtrfv
   13. pmtrprfv
   14. pmtrprfv3
   15. pmtrf
   16. pmtrmvd
   17. pmtrrn
   18. pmtrfrn
   19. pmtrffv
   20. pmtrrn2
   21. pmtrfinv
   22. pmtrfmvdn0
   23. pmtrff1o
   24. pmtrfcnv
   25. pmtrfb
   26. pmtrfconj
   27. symgsssg
   28. symgfisg
   29. symgtrf
   30. symggen
   31. symggen2
   32. symgtrinv
   33. pmtr3ncomlem1
   34. pmtr3ncomlem2
   35. pmtr3ncom
   36. pmtrdifellem1
   37. pmtrdifellem2
   38. pmtrdifellem3
   39. pmtrdifellem4
   40. pmtrdifel
   41. pmtrdifwrdellem1
   42. pmtrdifwrdellem2
   43. pmtrdifwrdellem3
   44. pmtrdifwrdel2lem1
   45. pmtrdifwrdel
   46. pmtrdifwrdel2
   47. pmtrprfval
   48. pmtrprfvalrn
5. The sign of a permutation
   1. cpsgn
   2. cevpm
   3. df-psgn
   4. df-evpm
   5. psgnunilem1
   6. psgnunilem5
   7. psgnunilem2
   8. psgnunilem3
   9. psgnunilem4
   10. m1expaddsub
   11. psgnuni
   12. psgnfval
   13. psgnfn
   14. psgndmsubg
   15. psgneldm
   16. psgneldm2
   17. psgneldm2i
   18. psgneu
   19. psgnval
   20. psgnvali
   21. psgnvalii
   22. psgnpmtr
   23. psgn0fv0
   24. sygbasnfpfi
   25. psgnfvalfi
   26. psgnvalfi
   27. psgnran
   28. gsmtrcl
   29. psgnfitr
   30. psgnfieu
   31. pmtrsn
   32. psgnsn
   33. psgnprfval
   34. psgnprfval1
   35. psgnprfval2