Metamath Proof Explorer


Table of Contents - 10.2.10. Symmetric groups

  1. Definition and basic properties
    1. csymg
    2. df-symg
    3. symgval
    4. permsetex
    5. symgbas
    6. symgbasex
    7. elsymgbas2
    8. elsymgbas
    9. symgbasf1o
    10. symgbasf
    11. symgbasmap
    12. symghash
    13. symgbasfi
    14. symgfv
    15. symgfvne
    16. symgressbas
    17. symgplusg
    18. symgov
    19. symgcl
    20. idresperm
    21. symgmov1
    22. symgmov2
    23. symgbas0
    24. symg1hash
    25. symg1bas
    26. symg2hash
    27. symg2bas
    28. 0symgefmndeq
    29. snsymgefmndeq
    30. symgpssefmnd
    31. symgvalstruct
    32. symgsubmefmnd
    33. symgtset
    34. symggrp
    35. symgid
    36. symginv
    37. symgsubmefmndALT
    38. galactghm
    39. lactghmga
    40. symgtopn
    41. symgga
    42. pgrpsubgsymgbi
    43. pgrpsubgsymg
    44. idressubgsymg
    45. 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