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

[Merged by Bors] - feat(category_theory/opposites): iso.unop #7400

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(category_theory/opposites): iso.unop #7400

wants to merge 5 commits into from

Conversation

jcommelin
Copy link
Member

Open in Gitpod

@jcommelin jcommelin added the awaiting-review The author would like community review of the PR label Apr 28, 2021
b-mehta
b-mehta reviewed Apr 28, 2021
View reviewed changes
src/category_theory/opposites.lean Outdated Show resolved Hide resolved
src/category_theory/opposites.lean Outdated Show resolved Hide resolved
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 29, 2021
@jcommelin jcommelin added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 4, 2021
b-mehta
b-mehta approved these changes May 4, 2021
View reviewed changes
Copy link
Collaborator

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

src/category_theory/opposites.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented May 4, 2021

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin @b-mehta
Update src/category_theory/opposites.lean
d8dae00 
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@jcommelin
Copy link
Member Author

bors merge

bors bot pushed a commit that referenced this pull request May 4, 2021
@jcommelin
feat(category_theory/opposites): iso.unop (#7400)
a573504
@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. 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 May 4, 2021
@bors
Copy link

bors bot commented May 4, 2021

This PR was included in a batch that timed out, it will be automatically retried

@bryangingechen
Copy link
Collaborator

bors r-
bors r+

@bors
Copy link

bors bot commented May 4, 2021

Canceled.

bors bot pushed a commit that referenced this pull request May 4, 2021
@jcommelin
feat(category_theory/opposites): iso.unop (#7400)
3c60ce3
@bors
Copy link

bors bot commented May 5, 2021

This PR was included in a batch that timed out, it will be automatically retried

@bryangingechen
Copy link
Collaborator

bors r-
bors r+

@bors
Copy link

bors bot commented May 5, 2021

Canceled.

bors bot pushed a commit that referenced this pull request May 5, 2021
@jcommelin
feat(category_theory/opposites): iso.unop (#7400)
78f6ab6
bors bot pushed a commit that referenced this pull request May 5, 2021
@jcommelin
feat(category_theory/opposites): iso.unop (#7400)
bb9216c
@bors
Copy link

bors bot commented May 5, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/opposites): iso.unop [Merged by Bors] - feat(category_theory/opposites): iso.unop May 5, 2021
@bors bors bot closed this May 5, 2021
@bors bors bot deleted the jcommelin-patch-2 branch May 5, 2021 18:50
Vierkantor pushed a commit that referenced this pull request May 6, 2021
@jcommelin @Vierkantor
feat(category_theory/opposites): iso.unop (#7400)
836d17c
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@b-mehta b-mehta b-mehta approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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.
4 participants
@jcommelin @bryangingechen @b-mehta @eric-wieser