Metamath Proof Explorer


Table of Contents - 21.50.18.5. The category of non-unital rings (alternate definition)

As an alternative to df-rngc, the "category of non-unital rings" can be defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, according to dfrngc2.

  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