Skip to content

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

Closed
eric-wieser wants to merge 36 commits intomasterfrom
eric-wieser/sym2-lemmas
Closed

[Merged by Bors] - feat: basic results about Finset.sym2#14212
eric-wieser wants to merge 36 commits intomasterfrom
eric-wieser/sym2-lemmas

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

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

@eric-wieser eric-wieser added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-combinatorics Combinatorics labels Jun 28, 2024
@github-actions
Copy link
Copy Markdown

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
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 28, 2024
@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
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 30, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 11, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 11, 2024

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
Copy Markdown
Contributor

@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

@eric-wieser eric-wieser requested a review from YaelDillies July 12, 2024 12:09
YaelDillies
YaelDillies approved these changes Jul 12, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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
Copy link
Copy Markdown

github-actions bot commented Jul 12, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 12, 2024
jcommelin
jcommelin reviewed Jul 12, 2024
View reviewed changes
Copy link
Copy Markdown
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

@ghost ghost 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
Copy Markdown
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
Copy Markdown
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 A reviewer has approved the changed; awaiting maintainer approval. 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.

4 participants

@eric-wieser @jcommelin @YaelDillies @kim-em