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
2. Ring unit
   1. cur
   2. df-ur
   3. ringidval
   4. dfur2
   5. Semirings
   6. The binomial theorem for semirings
3. Definition and basic properties of 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. ringi
   18. ringcl
   19. crngcom
   20. iscrng2
   21. ringass
   22. ringideu
   23. ringdi
   24. ringdir
   25. ringidcl
   26. ring0cl
   27. ringidmlem
   28. ringlidm
   29. ringridm
   30. isringid
   31. ringid
   32. ringadd2
   33. rngo2times
   34. ringidss
   35. ringacl
   36. ringcom
   37. ringabl
   38. ringcmn
   39. ringpropd
   40. crngpropd
   41. ringprop
   42. isringd
   43. iscrngd
   44. ringlz
   45. ringrz
   46. ringsrg
   47. ring1eq0
   48. ring1ne0
   49. ringinvnz1ne0
   50. ringinvnzdiv
   51. ringnegl
   52. rngnegr
   53. ringmneg1
   54. ringmneg2
   55. ringm2neg
   56. ringsubdi
   57. rngsubdir
   58. mulgass2
   59. ring1
   60. ringn0
   61. ringlghm
   62. ringrghm
   63. gsummulc1
   64. gsummulc2
   65. gsummgp0
   66. gsumdixp
   67. prdsmgp
   68. prdsmulrcl
   69. prdsringd
   70. prdscrngd
   71. prds1
   72. pwsring
   73. pws1
   74. pwscrng
   75. pwsmgp
   76. imasring
   77. qusring2
   78. crngbinom
4. 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. opprring
   14. opprringb
   15. oppr0
   16. oppr1
   17. opprneg
   18. opprsubg
   19. mulgass3
5. 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. cdvr
   46. df-dvr
   47. dvrfval
   48. dvrval
   49. dvrcl
   50. unitdvcl
   51. dvrid
   52. dvr1
   53. dvrass
   54. dvrcan1
   55. dvrcan3
   56. dvreq1
   57. ringinvdv
   58. rngidpropd
   59. dvdsrpropd
   60. unitpropd
   61. invrpropd
   62. isirred
   63. isnirred
   64. isirred2
   65. opprirred
   66. irredn0
   67. irredcl
   68. irrednu
   69. irredn1
   70. irredrmul
   71. irredlmul
   72. irredmul
   73. irredneg
   74. irrednegb
6. Ring primes
   1. crpm
   2. df-rprm
7. Ring homomorphisms
   1. crh
   2. crs
   3. cric
   4. df-rnghom
   5. df-rngiso
   6. dfrhm2
   7. df-ric
   8. rhmrcl1
   9. rhmrcl2
   10. isrhm
   11. rhmmhm
   12. isrim0
   13. rimrcl
   14. rhmghm
   15. rhmf
   16. rhmmul
   17. isrhm2d
   18. isrhmd
   19. rhm1
   20. idrhm
   21. rhmf1o
   22. isrim
   23. rimf1o
   24. rimrhm
   25. rimgim
   26. rhmco
   27. pwsco1rhm
   28. pwsco2rhm
   29. f1ghm0to0
   30. f1rhm0to0ALT
   31. gim0to0
   32. kerf1ghm
   33. brric
   34. brric2
   35. ricgic