Metamath Proof Explorer


Table of Contents - 10.2.10.4. Transpositions in the symmetric group

Transpositions are special cases of "cycles" as defined in [Rotman] p. 28: "Let i<sub>1</sub> , i<sub>2</sub> , ... , i<sub>r</sub> be distinct integers between 1 and n. If &alpha; in S<sub>n</sub> fixes the other integers and &alpha;(i<sub>1</sub>) = i<sub>2</sub>, &alpha;(i<sub>2</sub>) = i<sub>3</sub>, ..., &alpha;(i<sub>r-1</sub> ) = i<sub>r</sub>, &alpha;(i<sub>r</sub>) = i<sub>1</sub>, then &alpha; is an <b>r-cycle</b>. We also say that &alpha; is a cycle of <b>length</b> r." and in [Rotman] p. 31: "A 2-cycle is also called <b>transposition</b>.". <br><br> We (currently) do not have/need a definition for cycles, so transpositions are explicitly defined in df-pmtr.

  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