Terminology: unify names for ring unit

[avekens]

See also discussion in PR #4509:

We have several different names for 1r already at the beginning of section "Ring unit":

• ring unit (in comment for cur) - used 16 times in set.mm
• multiplicative neutral element of a ring (in comment for ~df-ur) - used 8 times in set.mm
• unity element of a ring (in comment for ~ringidval) - used 3 times in set.mm ("unity" only ist used 23 times)
• multiplicative identity (of a ring) (in comment of ~dfur2) - used 18 times in set.mm
• ring unity (in comment of ~pridln1) - used 2 times in set.mm

We should choose one of them as the name we will use primarily, and should mention the others in the comment of the definition.

In Wikipedia (see https://en.wikipedia.org/wiki/Identity_element ), "the identity with respect to multiplication is called a multiplicative identity (often denoted as 1)".
But also "The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity)."
A "unit", in contrast, is "an invertible element for the multiplication of the ring", see also definition of a "ring unit" Unit ( ~df-unit) in section "Divisibility", which is already an inconsistency within set.mm.

Therefore, I would propose to call it primarily "multiplicative identity" and alternatively "unity" or "unity element".

Consequently, the labes cur, df-ur and dfur2 should be changed, too. Maybe in

• cmid, df-mid, dfmid2 with "mid" for "multiplictive identity" (df-mi is already used!)
• or cue, df-ue, dfue2 with "ue" for "unity element"
• or c1r, df-1r, df1r2 analogous to the labels for 0g (I would prefer this variant)

[tirix]

I agree with the direction!
The 1r based labels would also be my preferred option.

[jkingdon]

Thanks for digging into this. I also would have said "multiplicative identity" so glad to hear that seems to be borne out by the sources you consulted.

As for "unit", the situation is worse than I thought, as some of the existing uses seem to be misapplying the word as you note.

[avekens]

I had a look at the literature, and saw that there is no uniform or even preferred terminology:

• N.Bourbaki and Marshall Hall call the multiplicative identity "unit" or "unit element"
• Steven Roman and Beauregard & Fraleigh call an invertible element a "unit"
• Serge Lang calls the multiplicative identity "unit element" and an invertible element a "unit"

In Wikipedia Unit (ring theory):

In algebra, a unit or invertible element of a ring is an invertible element for the multiplication of the ring. That is, an element u of a ring R is a unit if there exists v in R such that v u = u v = 1 , where 1 is the multiplicative identity;

and

Less commonly, the term unit is sometimes used to refer to the element 1 of the ring, in expressions like ring with a unit or unit ring, and also unit matrix. Because of this ambiguity, 1 is more commonly called the "unity" or the "identity" of the ring, and the phrases "ring with unity" or a "ring with identity" may be used to emphasize that one is considering a ring instead of a rng.

To avoid the ambiguity of the term "unit", I still propose to change the naming in (i)set.mm as discussed above.

[avekens]

Consequently, the labes cur, df-ur and dfur2 should be changed, too. Maybe in

* cmid, df-mid, dfmid2 with "mid" for "multiplictive identity" (df-mi is already used!)
* or cue, df-ue, dfue2 with "ue" for "unity element"
* or c1r, df-1r, df1r2 analogous to the labels for `0g` (I would prefer this variant)

Unfortunately, c1r and df-1r are used already (for signed real constant 1). And "ur" still stands for "Unity element in a Ring"). Therefore, I will not change the label...

[jkingdon]

Is this issue ready to close now that #4584 is merged, or is there more to be done?