Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(set_theory/ordinal/basic): max a 0 = a #13734

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(set_theory/ordinal/basic): max a 0 = a #13734

wants to merge 3 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Apr 27, 2022

Open in Gitpod

@vihdzp vihdzp added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Apr 27, 2022
@vihdzp vihdzp mentioned this pull request Apr 27, 2022
Closed
1 task
@kim-em
Copy link
Collaborator

kim-em commented Apr 28, 2022

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 28, 2022
bors bot pushed a commit that referenced this pull request Apr 28, 2022
@vihdzp
feat(set_theory/ordinal/basic): max a 0 = a (#13734)
0cb20fc
@bors
Copy link

bors bot commented Apr 28, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(set_theory/ordinal/basic): max a 0 = a [Merged by Bors] - feat(set_theory/ordinal/basic): max a 0 = a Apr 28, 2022
@bors bors bot closed this Apr 28, 2022
@bors bors bot deleted the max_zero branch April 28, 2022 09:22
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@vihdzp @kim-em