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,finset}/basic): card_erase_eq_ite #9185

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(data/{multiset,finset}/basic): card_erase_eq_ite #9185

wants to merge 10 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Sep 13, 2021 •
edited

A generic theorem about the cardinality of a finset or multiset with an element erased.

Open in Gitpod

Zulip thread

BoltonBailey and others added 2 commits September 13, 2021 13:16
@BoltonBailey @eric-wieser
Update src/data/finset/basic.lean
6eaa4e0 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@BoltonBailey
added to multiset
354007c
@BoltonBailey BoltonBailey changed the title feat(data/finset/basic): card_erase feat(data/{multiset,finset}/basic): card_erase_eq_ite Sep 13, 2021
@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Sep 18, 2021
@BoltonBailey @bryangingechen
Update src/data/multiset/basic.lean
ea531b3 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@urkud
Copy link
Member

urkud commented Sep 20, 2021

Thanks! 🎉
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 Sep 20, 2021
bors bot pushed a commit that referenced this pull request Sep 20, 2021
@BoltonBailey @eric-wieser
feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185)
976b261 
A generic theorem about the cardinality of a `finset` or `multiset` with an element erased.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Sep 20, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/{multiset,finset}/basic): card_erase_eq_ite [Merged by Bors] - feat(data/{multiset,finset}/basic): card_erase_eq_ite Sep 20, 2021
@bors bors bot closed this Sep 20, 2021
@bors bors bot deleted the BoltonBailey/card-erase branch September 20, 2021 06:29
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 left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@YaelDillies YaelDillies YaelDillies left review comments

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.

None yet
5 participants
@BoltonBailey @urkud @eric-wieser @bryangingechen @YaelDillies