Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unification of terms "ring unit" resp. "multiplicative identity" #4584

Merged
merged 7 commits into from
Jan 21, 2025

Conversation

avekens
Copy link
Contributor

@avekens avekens commented Jan 19, 2025

According to issue #4512, we have several different names for 1r already at the beginning of section "Ring unit". With this PR, these differences should be levelled out.
As proposed (and decided in principle) in issue #4512, 1r should be called "multiplicative identity" or "(ring) unity" or "unity element" uniformly in (i)set.mm.

An overview over the terms used in literature, and a discussion about the ambiguity of the term "unit" in the context of rings, is contained in the header comment of the section "Ring unit", which is changed to "Ring unity (multiplicative identity)" (see first commit).

In the following commits, the comments in set.mm are revised. I will do the same with iset.mm after this PR is accepted and merged (to avoid the effort to modify two files simultaneously if there are review remarks).

Here the details (provided in separate commits):

  • Title and header of section "Ring unit" -> "Ring Unity" (including addition of bibliographic reference [BeauregardFraleigh])
  • Replacement of "unit" by "unity" in comments (contains most of the changes)
  • lattice unit replaced (Two meanings: (Hilbert) lattice one and lattice unity)
  • unitary ring -> unital ring
  • nonunital -> non-unital
  • multiplicative neutral element -> unity element

* Explanation of ambiguity of the term "unit" and convention for using the terms "unit", "ring unity" and "multiplicative identity".
* bibliographic referenc  [BeauregardFraleigh] added
... and other minor changes in comments.
Two meanings:
* (Hilbert) lattice one
* lattice unity
and "neutral element" -> "zero element" (in the context of rings)
@avekens
Copy link
Contributor Author

avekens commented Jan 19, 2025

I think the level of section "Semirings" is wrong (currently subsubsection of "Ring unity (multiplicative identity)", formerly "Ring unit").
It should be a subsection of section 10.3 Rings. I will change this in the next commit.

Copy link
Contributor

@jkingdon jkingdon left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To be honest, I'm not completely sure what the "best" term to adopt is (if there even is such a thing), but this is clearly an improvement over what we had.

@wlammen wlammen merged commit de4cf63 into metamath:develop Jan 21, 2025
10 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants