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)).