Metamath Proof Explorer

Table of Contents - 21.50.18. Rings (extension)

  1. Nonzero rings (extension)
    1. lmod0rng
    2. nzrneg1ne0
  2. Ideals as non-unital rings
    1. lidldomn1
    2. lidlabl
    3. lidlrng
    4. zlidlring
    5. uzlidlring
    6. lidldomnnring
  3. The non-unital ring of even integers
    1. 0even
    2. 1neven
    3. 2even
    4. 2zlidl
    5. 2zrng
    6. 2zrngbas
    7. 2zrngadd
    8. 2zrng0
    9. 2zrngamgm
    10. 2zrngasgrp
    11. 2zrngamnd
    12. 2zrngacmnd
    13. 2zrngagrp
    14. 2zrngaabl
    15. 2zrngmul
    16. 2zrngmmgm
    17. 2zrngmsgrp
    18. 2zrngALT
    19. 2zrngnmlid
    20. 2zrngnmrid
    21. 2zrngnmlid2
    22. 2zrngnring
  4. A constructed not unital ring
    1. cznrnglem
    2. cznabel
    3. cznrng
    4. cznnring
  5. The category of non-unital rings (alternate definition)
    1. crngcALTV
    2. df-rngcALTV
    3. rngcvalALTV
    4. rngcbasALTV
    5. rngchomfvalALTV
    6. rngchomALTV
    7. elrngchomALTV
    8. rngccofvalALTV
    9. rngccoALTV
    10. rngccatidALTV
    11. rngccatALTV
    12. rngcidALTV
    13. rngcsectALTV
    14. rngcinvALTV
    15. rngcisoALTV
    16. rngchomffvalALTV
    17. rngchomrnghmresALTV
    18. rngcrescrhmALTV
    19. rhmsubcALTVlem1
    20. rhmsubcALTVlem2
    21. rhmsubcALTVlem3
    22. rhmsubcALTVlem4
    23. rhmsubcALTV
    24. rhmsubcALTVcat
  6. The category of (unital) rings (alternate definition)
    1. cringcALTV
    2. df-ringcALTV
    3. ringcvalALTV
    4. funcringcsetcALTV2lem1
    5. funcringcsetcALTV2lem2
    6. funcringcsetcALTV2lem3
    7. funcringcsetcALTV2lem4
    8. funcringcsetcALTV2lem5
    9. funcringcsetcALTV2lem6
    10. funcringcsetcALTV2lem7
    11. funcringcsetcALTV2lem8
    12. funcringcsetcALTV2lem9
    13. funcringcsetcALTV2
    14. ringcbasALTV
    15. ringchomfvalALTV
    16. ringchomALTV
    17. elringchomALTV
    18. ringccofvalALTV
    19. ringccoALTV
    20. ringccatidALTV
    21. ringccatALTV
    22. ringcidALTV
    23. ringcsectALTV
    24. ringcinvALTV
    25. ringcisoALTV
    26. ringcbasbasALTV
    27. funcringcsetclem1ALTV
    28. funcringcsetclem2ALTV
    29. funcringcsetclem3ALTV
    30. funcringcsetclem4ALTV
    31. funcringcsetclem5ALTV
    32. funcringcsetclem6ALTV
    33. funcringcsetclem7ALTV
    34. funcringcsetclem8ALTV
    35. funcringcsetclem9ALTV
    36. funcringcsetcALTV
    37. srhmsubcALTVlem1
    38. srhmsubcALTVlem2
    39. srhmsubcALTV
    40. sringcatALTV
    41. crhmsubcALTV
    42. cringcatALTV
    43. drhmsubcALTV
    44. drngcatALTV
    45. fldcatALTV
    46. fldcALTV
    47. fldhmsubcALTV