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.

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

[Merged by Bors] - feat: Create a partition from an element of Sym #14749

Closed
wants to merge 6 commits into from

Conversation

SashaIr
Copy link
Collaborator

@SashaIr SashaIr commented Jul 15, 2024

An element of Sym induces a partition given by the multiplicities of its elements.

Co-authored-by: Nirvana Coppola [email protected]


See #12572.

Open in Gitpod

@SashaIr SashaIr requested a review from YaelDillies July 15, 2024 08:43
@SashaIr SashaIr assigned SashaIr and unassigned SashaIr Jul 15, 2024
@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 15, 2024
Copy link

github-actions bot commented Jul 15, 2024

PR summary 021afbfb95

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ofSym
+ ofSymShapeEquiv
+ ofSym_map
+ ofSym_one
+ oneEquiv

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>

Mathlib/Combinatorics/Enumerative/Partition.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Enumerative/Partition.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Enumerative/Partition.lean Outdated Show resolved Hide resolved
Mathlib/Data/Sym/Basic.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 18, 2024
@SashaIr SashaIr removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 18, 2024
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 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 23, 2024
An element of Sym induces a partition given by the multiplicities of its elements.

Co-authored-by: Nirvana Coppola [[email protected]](mailto:[email protected])
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Create a partition from an element of Sym [Merged by Bors] - feat: Create a partition from an element of Sym Jul 23, 2024
@mathlib-bors mathlib-bors bot closed this Jul 23, 2024
@mathlib-bors mathlib-bors bot deleted the sashair-partitions-of-sym branch July 23, 2024 15:36
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants