There was a discussion at GitHub (issue #866 <https://github.com/metamath/set.mm/issues/866>) with the following result:
Definition: df-zzring $a |- ZZring = ( CCfld |``s ZZ ) Symbol: ℤring (althtmldef "ZZring" as "ℤ<SUB>ring</SUB>"; ): These will be availble in set.mm soon. On Thursday, May 30, 2019 at 8:25:58 AM UTC+2, Alexander van der Vekens wrote: > > 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 > <https://github.com/metamath/set.mm/issues/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? > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0da9603d-982b-49a2-970a-d8e0d8822b28%40googlegroups.com.
