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: (s ∩ t).card = s.card + t.card - (s ∪ t).card #10224

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card #10224

wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Feb 3, 2024 •
edited

once coerced to an AddGroupWithOne. Also unify Finset.card_disjoint_union and Finset.card_union_eq

From LeanAPAP

Open in Gitpod

@YaelDillies
feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card
6c5a63b 
once coerced to an `AddGroupWithOne`. Also unify `Finset.card_disjoint_union` and `Finset.card_union_eq`
@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Feb 3, 2024
@sgouezel sgouezel 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 Feb 9, 2024
@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 labels Feb 9, 2024
@Ruben-VandeVelde
Copy link
Collaborator

maintainer merge

@urkud urkud 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 Feb 11, 2024
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 11, 2024

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

@YaelDillies
Copy link
Collaborator Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Feb 11, 2024
@YaelDillies
feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card (#10224)
80bf34f 
once coerced to an `AddGroupWithOne`. Also unify `Finset.card_disjoint_union` and `Finset.card_union_eq`

From LeanAPAP
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 11, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card [Merged by Bors] - feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card Feb 11, 2024
@mathlib-bors mathlib-bors bot closed this Feb 11, 2024
@mathlib-bors mathlib-bors bot deleted the cast_card_union branch February 11, 2024 23:14
@acmepjz
Copy link
Collaborator

acmepjz commented Feb 13, 2024

I think it's good to have Finset.card_union_eq_iff which states that (s ∪ t).card = s.card + t.card if and only if Disjoint s t.

@acmepjz acmepjz mentioned this pull request Feb 13, 2024
Closed
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@YaelDillies @dagurtomas
feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card (#10224)
df80f92 
once coerced to an `AddGroupWithOne`. Also unify `Finset.card_disjoint_union` and `Finset.card_union_eq`

From LeanAPAP
@YaelDillies YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Apr 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@YaelDillies @Ruben-VandeVelde @acmepjz @urkud @sgouezel