On Monday, January 6, 2020 at 12:59:53 AM UTC+1, Norman Megill wrote: > > On Sunday, January 5, 2020 at 4:22:13 PM UTC-5, Alexander van der Vekens > wrote: >> >> On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote: >> >> > Another, more important, change within labels would be to replace >>> everywhere "rng" with "ring". Indeed, "rng" might refer to "rngs", which >>> is a common name for non-unital rings (rings that lost the "i" of >>> "identity"). Therefore, it is ambiguous, and it might be more difficult >>> than in the "sqr" case to deduce from a simple inspection if the given >>> theorem refers to rngs or rings. >>> >>> In principle, I agree with your suggestion to replace "rng" by "ring" >> for theorems about unital rings (and `Ring` is unital in set.mm). There >> are about 140 labels of theorems (in Parts 10-16 - only these should be >> relevant) containing "rng", and I think most of them should be renamed >> according to your proposal. In June 2019, I replaced already some labels >> (in the context of introducing ZZring) on your advise. On the other hand, >> there were changes of labels, replacing "ring" by "rng" for relevant >> labels, in 2013/14. There must have been a reason for this. >> > > The reason was simply to be more consistent. We only had one type of > ring, and some places used "ring" while others used "rng". I changed them > to "rng", picking the shorter of the two choices. I didn't know about the > two spellings used in the literature for different kinds of rings. > > >> Especially the label for the definition of a (unital) Ring, df-rng, was >> changed from df-ring to df-rng (see also >> https://groups.google.com/d/msg/metamath/HDQXr196Yo0/KhDrxgnRBgAJ) in >> July 2017, which should be reverted. But the table of abbreviations >> contains "rng" as convention to be used for (unital!) rings... >> >> To continue the discussion, a separate thread should be opened for this >> topic (wasn't there a corresponding issue in GitHub?)! >> > > I'm fine with making these changes since there is an ambiguity to be > resolved, and it is good to conform somewhat more closely to math texts > when it is practical to do so. If no one else has an objection, I don't > think we need to open a separate thread. If you (BJ) want to create a PR > for this when you find it convenient, please do so and we will accept it. > > This special subtopic is tracked by GitHub issue #1389 now...
Alexander -- 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/3bcf180c-da3b-4fd7-96ce-7d9cb7fa33dc%40googlegroups.com.
