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

invertible ring elements #2005

Merged
merged 4 commits into from
Jul 3, 2024
Merged

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jul 1, 2024

In this PR we:

  • Define notions of left and right invertibility of ring elements and define invertible elements as those which are both left and right invertible.
  • We prove basic uniqueness properties of inverses.
  • We prove basic closure properties of invertibility.
  • We define the group of units of a ring.

Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: 42782870-79fd-49c6-9715-43fa51a24b46 -->
theories/Algebra/Rings/Ring.v Outdated Show resolved Hide resolved
theories/Algebra/Rings/Ring.v Outdated Show resolved Hide resolved
theories/Algebra/Rings/Ring.v Outdated Show resolved Hide resolved
@Alizter
Copy link
Collaborator Author

Alizter commented Jul 3, 2024

@jdchristensen I've done the changes you suggested and will merge when this is green.

@Alizter Alizter merged commit 093e98e into HoTT:master Jul 3, 2024
20 checks passed
@Alizter Alizter deleted the ps/rr/invertible_ring_elements branch July 3, 2024 12:14
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.

None yet

2 participants