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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(data/multiset/basic): multiset.coe_eq_singleton #15910

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(data/multiset/basic): multiset.coe_eq_singleton #15910

wants to merge 15 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Aug 7, 2022 •
edited by YaelDillies

@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 blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Aug 7, 2022
@vihdzp vihdzp mentioned this pull request Aug 7, 2022
Closed
1 task
@vihdzp vihdzp changed the title feat(data/multiset/basic): more lemmas on multisets feat(data/multiset/basic): more basic lemmas on multisets Aug 7, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 19, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@eric-wieser eric-wieser added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 15, 2022
@eric-wieser
Copy link
Member

This looks like it's picked up some conflicts where the version on master reordered the lemmas (presumably from your other PR)

@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 Sep 15, 2022
@YaelDillies YaelDillies 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 merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Jan 11, 2023
@YaelDillies YaelDillies changed the title feat(data/multiset/basic): more basic lemmas on multisets feat(data/multiset/basic): multiset.coe_eq_singleton Jan 11, 2023
eric-wieser
eric-wieser approved these changes Jan 13, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Jan 13, 2023
bors bot pushed a commit that referenced this pull request Jan 13, 2023
@vihdzp @YaelDillies
feat(data/multiset/basic): multiset.coe_eq_singleton (#15910)
1c65ae0 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Jan 13, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 13, 2023
@vihdzp @YaelDillies
feat(data/multiset/basic): multiset.coe_eq_singleton (#15910)
5180997 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Jan 13, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 13, 2023
@vihdzp @YaelDillies
feat(data/multiset/basic): multiset.coe_eq_singleton (#15910)
f318726 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Jan 13, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/multiset/basic): multiset.coe_eq_singleton [Merged by Bors] - feat(data/multiset/basic): multiset.coe_eq_singleton Jan 13, 2023
@bors bors bot closed this Jan 13, 2023
@YaelDillies YaelDillies deleted the multiset_lemmas branch January 13, 2023 08:55
@fpvandoorn fpvandoorn mentioned this pull request Jan 26, 2023
Closed
eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2023
@eric-wieser
chore: forward-port leanprover-community/mathlib#15910
cd25509
eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2023
@eric-wieser
chore: forward-port leanprover-community/mathlib#15910
37aac8e
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2023
@eric-wieser
chore: forward-port leanprover-community/mathlib#15910 (#2538)
7ca25b3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

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.

None yet
5 participants
@vihdzp @mathlib-dependent-issues-bot @eric-wieser @YaelDillies @leanprover-community-bot-assistant