Metamath Proof Explorer

Table of Contents - 10.3. Rings

1. Multiplicative Group
   1. cmgp
   2. df-mgp
   3. fnmgp
   4. mgpval
   5. mgpplusg
   6. mgplem
   7. mgpbas
   8. mgpsca
   9. mgptset
   10. mgptopn
   11. mgpds
   12. mgpress
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. ringmnd
   11. ringmgm
   12. crngring
   13. mgpf
   14. ringi
   15. ringcl
   16. crngcom
   17. iscrng2
   18. ringass
   19. ringideu
   20. ringdi
   21. ringdir
   22. ringidcl
   23. ring0cl
   24. ringidmlem
   25. ringlidm
   26. ringridm
   27. isringid
   28. ringid
   29. ringadd2
   30. rngo2times
   31. ringidss
   32. ringacl
   33. ringcom
   34. ringabl
   35. ringcmn
   36. ringpropd
   37. crngpropd
   38. ringprop
   39. isringd
   40. iscrngd
   41. ringlz
   42. ringrz
   43. ringsrg
   44. ring1eq0
   45. ring1ne0
   46. ringinvnz1ne0
   47. ringinvnzdiv
   48. ringnegl
   49. rngnegr
   50. ringmneg1
   51. ringmneg2
   52. ringm2neg
   53. ringsubdi
   54. rngsubdir
   55. mulgass2
   56. ring1
   57. ringn0
   58. ringlghm
   59. ringrghm
   60. gsummulc1
   61. gsummulc2
   62. gsummgp0
   63. gsumdixp
   64. prdsmgp
   65. prdsmulrcl
   66. prdsringd
   67. prdscrngd
   68. prds1
   69. pwsring
   70. pws1
   71. pwscrng
   72. pwsmgp
   73. imasring
   74. qusring2
   75. crngbinom
4. Opposite ring
   1. coppr
   2. df-oppr
   3. opprval
   4. opprmulfval
   5. opprmul
   6. crngoppr
   7. opprlem
   8. opprbas
   9. oppradd
   10. opprring
   11. opprringb
   12. oppr0
   13. oppr1
   14. opprneg
   15. opprsubg
   16. 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. f1rhm0to0OLD
   31. f1rhm0to0ALT
   32. gim0to0
   33. rim0to0OLD
   34. kerf1ghm
   35. kerf1hrmOLD
   36. brric
   37. brric2
   38. ricgic