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
   13. elmgplsm
   14. elmgplsmd
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
   30. rng1zrlem
   31. rng1zr
   32. rngen1zr
   33. rngen1zr0
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. srgen1zr0
   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. ringcld
   26. ringassd
   27. crng12d
   28. crng32d
   29. crng4
   30. ringdi
   31. ringdir
   32. ringdid
   33. ringdird
   34. ringdi22
   35. ringidcl
   36. ringidcld
   37. ring0cl
   38. ringidmlem
   39. ringlidm
   40. ringridm
   41. isringid
   42. ringlidmd
   43. ringridmd
   44. ringid
   45. ringo2times
   46. ringadd2
   47. ringidss
   48. ringacl
   49. ringcomlem
   50. ringcom
   51. ringabl
   52. ringcmn
   53. ringabld
   54. ringcmnd
   55. ringrng
   56. ringssrng
   57. isringrng
   58. dfring2
   59. ringpropd
   60. crngpropd
   61. ringprop
   62. isringd
   63. iscrngd
   64. ringlz
   65. ringrz
   66. ringlzd
   67. ringrzd
   68. ringsrg
   69. ring1eq0
   70. ring1ne0
   71. ringinvnz1ne0
   72. ringinvnzdiv
   73. ringnegl
   74. ringnegr
   75. ringmneg1
   76. ringmneg2
   77. ringm2neg
   78. ringsubdi
   79. ringsubdir
   80. mulgass2
   81. ring1
   82. ringn0
   83. ringlghm
   84. ringrghm
   85. gsummulc1
   86. gsummulc2
   87. gsummgp0
   88. gsumdixp
   89. prdsmulrcl
   90. prdsringd
   91. prdscrngd
   92. prds1
   93. pwsring
   94. pws1
   95. pwscrng
   96. pwsmgp
   97. pwspjmhmmgpd
   98. pwsexpg
   99. pwsgprod
   100. imasring
   101. imasringf1
   102. xpsringd
   103. xpsring1d
   104. qusring2
   105. 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. rhmval0
    8. isrhm0
    9. rhmrcl1
    10. rhmrcl2
    11. isrhm
    12. rhmmhm
    13. rhmisrnghm
    14. rimrcl
    15. isrim0
    16. rhmghm
    17. rhmf
    18. rhmcl
    19. rimcnv
    20. rhmadd
    21. rhmsub
    22. rhmmul
    23. isrhm2d
    24. isrhmd
    25. rhm0
    26. rhm1
    27. idrhm
    28. crngrhmfo
    29. rhmf1o
    30. isrim
    31. rimf1o
    32. rimval
    33. rimrhm
    34. rimrcl1
    35. rimrcl2
    36. rimgim
    37. rimisrngim
    38. rhmfn
    39. rimfn
    40. rhmval
    41. rhmco
    42. rhmkerinj
    43. pwsco1rhm
    44. pwsco2rhm
    45. df-ric
    46. ricrel
    47. brric
    48. brrici
    49. rimco
    50. ricref
    51. riclcl
    52. ricrcl
    53. ricsym
    54. rictr
    55. isbrric2
    56. brric2
    57. ricgic
    58. ricer
    59. rhmdvdsr
    60. rhmopp
    61. elrhmunit
    62. rhmunitinv
11. Nonzero rings and zero rings
    1. cnzr
    2. df-nzr
    3. isnzr
    4. nzrnz
    5. nzrring
    6. nzrringOLD
    7. isnzr2
    8. drnglidl1ne0
    9. isnzr2hash
    10. nzrpropd
    11. opprnzrb
    12. opprnzr
    13. ringelnzr
    14. nzrunit
    15. 0ringnnzr
    16. 0ring
    17. 0ringdif
    18. 0ringbas
    19. 0ring01eq
    20. 01eq0ring
    21. 01eq0ringOLD
    22. 0ring01eqbi2
    23. 0ring01eqbi
    24. 0ring1eq0
    25. c0rhm
    26. c0rnghm
    27. zrrnghm
    28. 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. domnrrg
    23. isdomn6
    24. isdomn3
    25. isdomn4
    26. opprdomnb
    27. opprdomn
    28. isdomn4r
    29. domnlcanb
    30. domnlcan
    31. domnrcanb
    32. domnrcan
    33. domneq0r
    34. isidom
    35. idomdomd
    36. idomcringd
    37. idomringd