Definition/Symbol for the ring of integers

[Alexander van der Vekens]

Recently I moved the section "The ordered commutative ring of integers" in TA's mathbox into the main part, as section "10.11.2 Ring of integers", see http://us2.metamath.org:88/mpeuni/mmtheorems176.html and also Issue #866 at GitHub. There is, however, not a definition of the ring of integers yet, but it is represented as restriction of the field of complex numbers ( CCfld |`s ZZ ) . Since, in my opinion, the "Ring of integers" is an important and central concept in mathematics, I think it deserves a particular definition.

My suggestion would be

df-rngz $a |- RingZ = ( CCfld |`s ZZ ) .

As symbol to be used in HTML we could use ℤ_rng (analogously to ℂ_fld for CCfld).

Unfortunately, there is already a definition df-zrng $a |- ZRing = ... in Mario's Mathbox (subring of integral elements in a ring), so ZRing cannot be used for the "Ring of integers" (or Mario's definition must be changed). Alternatively, we could use ZZRing or ZZRng or ZZrng (this is closest to CCfld) for the "Ring of integers".

What do you think about this? Which (of the proposed) class name(s) do you prefer?

[Alexander van der Vekens]

There was a discussion at GitHub (issue #866) with the following result:

Definition: df-zzring $a |- ZZring = ( CCfld |``s ZZ )
Symbol: ℤ_ring (althtmldef "ZZring" as "&#8484;<SUB>ring</SUB>"; ):

These will be availble in set.mm soon.