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

[Merged by Bors] - feat(algebra/big_operators/nat_antidiagonal): a few more lemmas #4783

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(algebra/big_operators/nat_antidiagonal): a few more lemmas #4783

wants to merge 1 commit into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Oct 25, 2020

@urkud urkud added the awaiting-review The author would like community review of the PR label Oct 26, 2020
bryangingechen
bryangingechen approved these changes Oct 26, 2020
View reviewed changes
Copy link
Collaborator

@bryangingechen bryangingechen 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 r+

@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 Oct 26, 2020
bors bot pushed a commit that referenced this pull request Oct 26, 2020
@urkud
feat(algebra/big_operators/nat_antidiagonal): a few more lemmas (#4783)
4036212
@bors
Copy link

bors bot commented Oct 26, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/big_operators/nat_antidiagonal): a few more lemmas [Merged by Bors] - feat(algebra/big_operators/nat_antidiagonal): a few more lemmas Oct 26, 2020
@bors bors bot closed this Oct 26, 2020
@bors bors bot deleted the nat-antidiagonal branch October 26, 2020 05:20
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@bryangingechen bryangingechen bryangingechen approved these changes

Assignees
No one assigned
Labels
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
@urkud @bryangingechen