Metamath Proof Explorer


Table of Contents - 10.10.2. Ring of integers

According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring ." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by , the field of complex numbers restricted to the integers. In zringring it is shown that this restriction is a ring (it is actually a principal ideal ring as shown in zringlpir), and zringbas shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as definition df-zring of the ring of integers.

Remark: Instead of using the symbol "ZZrng" analogous to used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra)).

  1. zring
  2. df-zring
  3. zringcrng
  4. zringring
  5. zringabl
  6. zringgrp
  7. zringbas
  8. zringplusg
  9. zringmulg
  10. zringmulr
  11. zring0
  12. zring1
  13. zringnzr
  14. dvdsrzring
  15. zringlpirlem1
  16. zringlpirlem2
  17. zringlpirlem3
  18. zringinvg
  19. zringunit
  20. zringlpir
  21. zringndrg
  22. zringcyg
  23. zringmpg
  24. prmirredlem
  25. dfprm2
  26. prmirred
  27. expghm
  28. mulgghm2
  29. mulgrhm
  30. mulgrhm2