Metamath Proof Explorer

Table of Contents - 10.3. Rings

1. Multiplicative Group
   1. cmgp
   2. df-mgp
   3. fnmgp
   4. mgpval
   5. mgpplusg
   6. mgpbas
   7. mgpsca
   8. mgptset
   9. mgptopn
   10. mgpds
   11. mgpress
   12. 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. crng32d
   28. ringcld
   29. ringdi
   30. ringdir
   31. ringdid
   32. ringdird
   33. ringidcl
   34. ringidcld
   35. ring0cl
   36. ringidmlem
   37. ringlidm
   38. ringridm
   39. isringid
   40. ringlidmd
   41. ringridmd
   42. ringid
   43. ringo2times
   44. ringadd2
   45. ringidss
   46. ringacl
   47. ringcomlem
   48. ringcom
   49. ringabl
   50. ringcmn
   51. ringabld
   52. ringcmnd
   53. ringrng
   54. ringssrng
   55. isringrng
   56. ringpropd
   57. crngpropd
   58. ringprop
   59. isringd
   60. iscrngd
   61. ringlz
   62. ringrz
   63. ringlzd
   64. ringrzd
   65. ringsrg
   66. ring1eq0
   67. ring1ne0
   68. ringinvnz1ne0
   69. ringinvnzdiv
   70. ringnegl
   71. ringnegr
   72. ringmneg1
   73. ringmneg2
   74. ringm2neg
   75. ringsubdi
   76. ringsubdir
   77. mulgass2
   78. ring1
   79. ringn0
   80. ringlghm
   81. ringrghm
   82. gsummulc1OLD
   83. gsummulc2OLD
   84. gsummulc1
   85. gsummulc2
   86. gsummgp0
   87. gsumdixp
   88. prdsmulrcl
   89. prdsringd
   90. prdscrngd
   91. prds1
   92. pwsring
   93. pws1
   94. pwscrng
   95. pwsmgp
   96. pwspjmhmmgpd
   97. pwsexpg
   98. imasring
   99. imasringf1
   100. xpsringd
   101. xpsring1d
   102. qusring2
   103. crngbinom
6. Opposite ring
   1. coppr
   2. df-oppr
   3. opprval
   4. opprmulfval
   5. opprmul
   6. crngoppr
   7. opprlem
   8. opprbas
   9. oppradd
   10. opprrng
   11. opprrngb
   12. opprring
   13. opprringb
   14. oppr0
   15. oppr1
   16. opprneg
   17. opprsubg
   18. 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. nzrpropd
    10. opprnzrb
    11. opprnzr
    12. ringelnzr
    13. nzrunit
    14. 0ringnnzr
    15. 0ring
    16. 0ringdif
    17. 0ringbas
    18. 0ring01eq
    19. 01eq0ring
    20. 01eq0ringOLD
    21. 0ring01eqbi
    22. 0ring1eq0
    23. c0rhm
    24. c0rnghm
    25. zrrnghm
    26. 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
    3. Subrings generated by a subset
14. Categories of rings
    1. The category of non-unital rings
    2. The category of (unital) rings
    3. Subcategories of the category of rings
15. Left regular elements and domains
    1. crlreg
    2. cdomn
    3. cidom
    4. df-rlreg
    5. df-domn
    6. df-idom
    7. rrgval
    8. isrrg
    9. rrgeq0i
    10. rrgeq0
    11. rrgsupp
    12. rrgss
    13. unitrrg
    14. rrgnz
    15. isdomn
    16. domnnzr
    17. domnring
    18. domneq0
    19. domnmuln0
    20. isdomn5
    21. isdomn2
    22. isdomn2OLD
    23. domnrrg
    24. isdomn6
    25. isdomn3
    26. isdomn4
    27. opprdomnb
    28. opprdomn
    29. isdomn4r
    30. domnlcanb
    31. domnlcan
    32. domnrcanb
    33. domnrcan
    34. domneq0r
    35. isidom
    36. idomdomd
    37. idomcringd
    38. idomringd