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: basic results about Finset.sym2 #14212

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat: basic results about Finset.sym2 #14212

wants to merge 36 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jun 28, 2024 •
edited
Loading

@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 28, 2024 •
edited
Loading

PR summary c2f79efa3e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _root_.Function.Embedding.sym2Map
+ map_mk_disjoint_sym2
+ map_mk_sublist_sym2
+ mkEmbedding
+ sym2_image
+ sym2_insert
+ sym2_zero
++ dedup_sym2
++ sym2_cons
+++ sym2_map

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@eric-wieser eric-wieser mentioned this pull request Jun 28, 2024
Closed
1 task
@eric-wieser eric-wieser requested a review from kmill June 28, 2024 01:32
@eric-wieser eric-wieser changed the title feat: add results about Finset.cons and Finset.sym2 feat: basic results about Finset.sym2 Jun 28, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 11, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@eric-wieser eric-wieser requested a review from urkud July 11, 2024 14:49
YaelDillies
YaelDillies approved these changes Jul 12, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Otherwise looks good

Mathlib/Data/Finset/Sym.lean Outdated Show resolved Hide resolved
Mathlib/Data/List/Sym.lean Outdated Show resolved Hide resolved
Mathlib/Data/List/Sym.lean Outdated Show resolved Hide resolved
YaelDillies
YaelDillies approved these changes Jul 12, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Nice that you finally cracked the dedup_sym2 nut!

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin
jcommelin reviewed Jul 12, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin 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 merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@eric-wieser
feat: basic results about Finset.sym2 (#14212)
a029d7a
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 12, 2024

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

mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@eric-wieser
feat: basic results about Finset.sym2 (#14212)
2f97af5
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: basic results about Finset.sym2 [Merged by Bors] - feat: basic results about Finset.sym2 Jul 12, 2024
@mathlib-bors mathlib-bors bot closed this Jul 12, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/sym2-lemmas branch July 12, 2024 15:30
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

@kmill kmill Awaiting requested review from kmill

@urkud urkud Awaiting requested review from urkud

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@eric-wieser @leanprover-community-mathlib4-bot @jcommelin @YaelDillies @kim-em