Metamath Proof Explorer

Table of Contents - 10.3. Rings

1. Multiplicative Group
   1. cmgp
   2. df-mgp
   3. fnmgp
   4. mgpval
   5. mgpplusg
   6. mgplemOLD
   7. mgpbas
   8. mgpbasOLD
   9. mgpsca
   10. mgpscaOLD
   11. mgptset
   12. mgptsetOLD
   13. mgptopn
   14. mgpds
   15. mgpdsOLD
   16. mgpress
   17. mgpressOLD
   18. prdsmgp
2. Non-unital rings ("rngs")
   1. crng
   2. df-rng
   3. isrng
   4. rngabl
   5. rngmgp
   6. rngmgpf
   7. rnggrp
   8. rngass
   9. rngdi
   10. rngdir
   11. rngacl
   12. rng0cl
   13. rngcl
   14. rnglz
   15. rngrz
   16. rngmneg1
   17. rngmneg2
   18. rngm2neg
   19. rngansg
   20. rngsubdi
   21. rngsubdir
   22. isrngd
   23. rngpropd
   24. prdsmulrngcl
   25. prdsrngd
   26. imasrng
   27. imasrngf1
   28. xpsrngd
   29. qusrng
3. Ring unity (multiplicative identity)
   1. cur
   2. df-ur
   3. ringidval
   4. dfur2
   5. ringurd
4. Semirings
   1. csrg
   2. df-srg
   3. issrg
   4. srgcmn
   5. srgmnd
   6. srgmgp
   7. srgdilem
   8. srgcl
   9. srgass
   10. srgideu
   11. srgfcl
   12. srgdi
   13. srgdir
   14. srgidcl
   15. srg0cl
   16. srgidmlem
   17. srglidm
   18. srgridm
   19. issrgid
   20. srgacl
   21. srgcom
   22. srgrz
   23. srglz
   24. srgisid
   25. o2timesd
   26. rglcom4d
   27. srgo2times
   28. srgcom4lem
   29. srgcom4
   30. srg1zr
   31. srgen1zr
   32. srgmulgass
   33. srgpcomp
   34. srgpcompp
   35. srgpcomppsc
   36. srglmhm
   37. srgrmhm
   38. srgsummulcr
   39. sgsummulcl
   40. srg1expzeq1
   41. The binomial theorem for semirings
5. Unital rings
   1. crg
   2. ccrg
   3. df-ring
   4. df-cring
   5. isring
   6. ringgrp
   7. ringmgp
   8. iscrng
   9. crngmgp
   10. ringgrpd
   11. ringmnd
   12. ringmgm
   13. crngring
   14. crngringd
   15. crnggrpd
   16. mgpf
   17. ringdilem
   18. ringcl
   19. crngcom
   20. iscrng2
   21. ringass
   22. ringideu
   23. crngcomd
   24. crngbascntr
   25. ringassd
   26. crng12d
   27. ringcld
   28. ringdi
   29. ringdir
   30. ringidcl
   31. ring0cl
   32. ringidmlem
   33. ringlidm
   34. ringridm
   35. isringid
   36. ringlidmd
   37. ringridmd
   38. ringid
   39. ringo2times
   40. ringadd2
   41. ringidss
   42. ringacl
   43. ringcomlem
   44. ringcom
   45. ringabl
   46. ringcmn
   47. ringabld
   48. ringcmnd
   49. ringrng
   50. ringssrng
   51. isringrng
   52. ringpropd
   53. crngpropd
   54. ringprop
   55. isringd
   56. iscrngd
   57. ringlz
   58. ringrz
   59. ringlzd
   60. ringrzd
   61. ringsrg
   62. ring1eq0
   63. ring1ne0
   64. ringinvnz1ne0
   65. ringinvnzdiv
   66. ringnegl
   67. ringnegr
   68. ringmneg1
   69. ringmneg2
   70. ringm2neg
   71. ringsubdi
   72. ringsubdir
   73. mulgass2
   74. ring1
   75. ringn0
   76. ringlghm
   77. ringrghm
   78. gsummulc1OLD
   79. gsummulc2OLD
   80. gsummulc1
   81. gsummulc2
   82. gsummgp0
   83. gsumdixp
   84. prdsmulrcl
   85. prdsringd
   86. prdscrngd
   87. prds1
   88. pwsring
   89. pws1
   90. pwscrng
   91. pwsmgp
   92. pwspjmhmmgpd
   93. pwsexpg
   94. imasring
   95. imasringf1
   96. xpsringd
   97. xpsring1d
   98. qusring2
   99. crngbinom
6. Opposite ring
   1. coppr
   2. df-oppr
   3. opprval
   4. opprmulfval
   5. opprmul
   6. crngoppr
   7. opprlem
   8. opprlemOLD
   9. opprbas
   10. opprbasOLD
   11. oppradd
   12. oppraddOLD
   13. opprrng
   14. opprrngb
   15. opprring
   16. opprringb
   17. oppr0
   18. oppr1
   19. opprneg
   20. opprsubg
   21. mulgass3
7. Divisibility
   1. cdsr
   2. cui
   3. cir
   4. df-dvdsr
   5. df-unit
   6. df-irred
   7. reldvdsr
   8. dvdsrval
   9. dvdsr
   10. dvdsr2
   11. dvdsrmul
   12. dvdsrcl
   13. dvdsrcl2
   14. dvdsrid
   15. dvdsrtr
   16. dvdsrmul1
   17. dvdsrneg
   18. dvdsr01
   19. dvdsr02
   20. isunit
   21. 1unit
   22. unitcl
   23. unitss
   24. opprunit
   25. crngunit
   26. dvdsunit
   27. unitmulcl
   28. unitmulclb
   29. unitgrpbas
   30. unitgrp
   31. unitabl
   32. unitgrpid
   33. unitsubm
   34. cinvr
   35. df-invr
   36. invrfval
   37. unitinvcl
   38. unitinvinv
   39. ringinvcl
   40. unitlinv
   41. unitrinv
   42. 1rinv
   43. 0unit
   44. unitnegcl
   45. ringunitnzdiv
   46. ring1nzdiv
   47. cdvr
   48. df-dvr
   49. dvrfval
   50. dvrval
   51. dvrcl
   52. unitdvcl
   53. dvrid
   54. dvr1
   55. dvrass
   56. dvrcan1
   57. dvrcan3
   58. dvreq1
   59. dvrdir
   60. rdivmuldivd
   61. ringinvdv
   62. rngidpropd
   63. dvdsrpropd
   64. unitpropd
   65. invrpropd
   66. isirred
   67. isnirred
   68. isirred2
   69. opprirred
   70. irredn0
   71. irredcl
   72. irrednu
   73. irredn1
   74. irredrmul
   75. irredlmul
   76. irredmul
   77. irredneg
   78. irrednegb
8. Ring primes
   1. crpm
   2. df-rprm
9. Homomorphisms of non-unital rings
   1. crnghm
   2. crngim
   3. df-rnghm
   4. df-rngim
   5. rnghmrcl
   6. rnghmfn
   7. rnghmval
   8. isrnghm
   9. isrnghmmul
   10. rnghmmgmhm
   11. rnghmval2
   12. isrngim
   13. rngimrcl
   14. rnghmghm
   15. rnghmf
   16. rnghmmul
   17. isrnghm2d
   18. isrnghmd
   19. rnghmf1o
   20. isrngim2
   21. rngimf1o
   22. rngimrnghm
   23. rngimcnv
   24. rnghmco
   25. idrnghm
   26. c0mgm
   27. c0mhm
   28. c0ghm
   29. c0snmgmhm
   30. c0snmhm
   31. c0snghm
   32. rngisomfv1
   33. rngisom1
   34. rngisomring
   35. rngisomring1
10. Ring homomorphisms
    1. crh
    2. crs
    3. cric
    4. df-rhm
    5. df-rim
    6. dfrhm2
    7. df-ric
    8. rhmrcl1
    9. rhmrcl2
    10. isrhm
    11. rhmmhm
    12. rhmisrnghm
    13. isrim0OLD
    14. rimrcl
    15. isrim0
    16. rhmghm
    17. rhmf
    18. rhmmul
    19. isrhm2d
    20. isrhmd
    21. rhm1
    22. idrhm
    23. rhmf1o
    24. isrim
    25. isrimOLD
    26. rimf1o
    27. rimrhmOLD
    28. rimrhm
    29. rimgim
    30. rimisrngim
    31. rhmfn
    32. rhmval
    33. rhmco
    34. pwsco1rhm
    35. pwsco2rhm
    36. brric
    37. brrici
    38. brric2
    39. ricgic
    40. rhmdvdsr
    41. rhmopp
    42. elrhmunit
    43. rhmunitinv
11. Nonzero rings and zero rings
    1. cnzr
    2. df-nzr
    3. isnzr
    4. nzrnz
    5. nzrring
    6. nzrringOLD
    7. isnzr2
    8. isnzr2hash
    9. opprnzr
    10. ringelnzr
    11. nzrunit
    12. 0ringnnzr
    13. 0ring
    14. 0ringdif
    15. 0ringbas
    16. 0ring01eq
    17. 01eq0ring
    18. 01eq0ringOLD
    19. 0ring01eqbi
    20. 0ring1eq0
    21. c0rhm
    22. c0rnghm
    23. zrrnghm
    24. nrhmzr
12. Local rings
    1. clring
    2. df-lring
    3. islring
    4. lringnzr
    5. lringring
    6. lringnz
    7. lringuplu
13. Subrings
    1. Subrings of non-unital rings
    2. Subrings of unital rings
14. Categories of rings
    1. The category of non-unital rings
    2. The category of (unital) rings
    3. Subcategories of the category of rings