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/1a918e90-9620-4d57-b4d0-e6827f421e77%40googlegroups.com.
