Hi Benoît On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote: > > Indeed, I think that BASIC also uses "sqr" for "square root", but for most > modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, so I > would prefer that in all labels, "sqr" be replaced with "sqrt". > > 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. 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?)! Alexander PS: Your recent changes of labels, especially impd and expd, are very helpful for me! -- 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/2c0b16bf-cf61-418a-ae85-854383e2eec5%40googlegroups.com.
