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(Combinatorics): definition and basic properties of Schnirelmann density #7342

Closed
wants to merge 11 commits into from

Conversation

b-mehta
Copy link
Contributor

@b-mehta b-mehta commented Sep 23, 2023

Provide the definition of the Schnirelmann density, basic properties of it, and some simple useful calculations.

Co-authored-by: Yaël Dillies yael.dillies@gmail.com
Co-authored-by: Doga Can Sertbas dogacan.sertbas@gmail.com


Open in Gitpod

@b-mehta b-mehta added awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Sep 23, 2023
Copy link
Member

@hrmacbeth hrmacbeth left a comment

Choose a reason for hiding this comment

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

A few uses of the new tactic gcongr, optional of course. To use them you will need to mark Finset.card_le_of_subset with @[gcongr], but that should be done in any case.

Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
@b-mehta b-mehta requested a review from a team October 1, 2023 21:13
Mathlib/Combinatorics/Schnirelmann.lean Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved

## References

Ruzsa, Imre. (2009). Sumsets and structure. Combinatorial Number Theory and Additive Group Theory.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could you add that to reference.bib?

@Article{         ruzsa2009,
  author        = {Ruzsa, Imre},
  title         = {Sumsets and structure},
  journal       = {Combinatorial Number Theory and Additive Group Theory},
  year          = {2009},
  month         = {01}
}

Copy link
Member

Choose a reason for hiding this comment

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

🏓

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@jcommelin
Copy link
Member

bors d+

Copy link

bors bot commented Nov 3, 2023

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

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Nov 3, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 8, 2023
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
Mathlib/Combinatorics/Schnirelmann.lean Outdated Show resolved Hide resolved
YaelDillies and others added 2 commits December 12, 2023 22:43
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 12, 2023
@jcommelin
Copy link
Member

bors d=YaelDillies

@mathlib-bors
Copy link

mathlib-bors bot commented Dec 13, 2023

✌️ 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

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Dec 13, 2023
…density (#7342)

Provide the definition of the Schnirelmann density, basic properties of it, and some simple useful calculations.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Doga Can Sertbas <dogacan.sertbas@gmail.com>



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 13, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Combinatorics): definition and basic properties of Schnirelmann density [Merged by Bors] - feat(Combinatorics): definition and basic properties of Schnirelmann density Dec 13, 2023
@mathlib-bors mathlib-bors bot closed this Dec 13, 2023
@mathlib-bors mathlib-bors bot deleted the schnirelmann branch December 13, 2023 09:14
awueth pushed a commit that referenced this pull request Dec 19, 2023
…density (#7342)

Provide the definition of the Schnirelmann density, basic properties of it, and some simple useful calculations.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Doga Can Sertbas <dogacan.sertbas@gmail.com>



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants