Skip to content

[Merged by Bors] - feat: forward direction of Turán's theorem#11990

Closed
Parcly-Taxel wants to merge 18 commits intomasterfrom
zykov
Closed

[Merged by Bors] - feat: forward direction of Turán's theorem#11990
Parcly-Taxel wants to merge 18 commits intomasterfrom
zykov

Conversation

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel commented Apr 7, 2024 •
edited
Loading

Part of #9317.

Open in Gitpod

@Parcly-Taxel Parcly-Taxel mentioned this pull request Apr 7, 2024
Closed
@fpvandoorn fpvandoorn removed their request for review April 7, 2024 17:27
@Parcly-Taxel Parcly-Taxel changed the title feat: Zykov symmetrisation, up to the finpartition feat: forward direction of Turán's theorem Jun 5, 2024
jcommelin
jcommelin reviewed Jun 5, 2024
View reviewed changes
@Parcly-Taxel Parcly-Taxel requested a review from jcommelin June 5, 2024 15:26
@Parcly-Taxel Parcly-Taxel requested review from YaelDillies and removed request for YaelDillies, jcommelin and kmill June 13, 2024 01:51
YaelDillies
YaelDillies reviewed Jun 17, 2024
View reviewed changes
@YaelDillies YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 17, 2024
@Parcly-Taxel Parcly-Taxel added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 19, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 9f59057bfe

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Combinatorics.SimpleGraph.Turan 506 578 +72 (+14.23%)

Declarations diff

+ card_parts
+ card_parts_le
+ degree_eq_card_sub_part_card
+ degree_eq_of_not_adj
+ equivalence_not_adj
+ exists_isTuranMaximal
+ finpartition
+ instance : DecidableRel h.setoid.r
+ isEquipartition
+ mem_part_iff_part_eq_part
+ nonempty_iso_turanGraph
+ not_adj_iff_part_eq
+ not_adj_trans
+ part_eq_of_mem
+ setoid

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

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

YaelDillies
YaelDillies reviewed Jun 19, 2024
View reviewed changes
@Parcly-Taxel @YaelDillies
Update Mathlib/Combinatorics/SimpleGraph/Turan.lean
0e0147b 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies approved these changes Jun 19, 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.

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 19, 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 Jun 19, 2024
kmill
kmill reviewed Jun 22, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@kmill kmill left a comment

Choose a reason for hiding this comment

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

Thanks! I have one comment, but that could be addressed later.

bors r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 22, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 22, 2024
@Parcly-Taxel
feat: forward direction of Turán's theorem (#11990)
2985a84 
Part of #9317.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 22, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: forward direction of Turán's theorem [Merged by Bors] - feat: forward direction of Turán's theorem Jun 22, 2024
@mathlib-bors mathlib-bors bot closed this Jun 22, 2024
@mathlib-bors mathlib-bors bot deleted the zykov branch June 22, 2024 19:24
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@Parcly-Taxel @kbuzzard
feat: forward direction of Turán's theorem (#11990)
ca263f4 
Part of #9317.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@Parcly-Taxel @dagurtomas
feat: forward direction of Turán's theorem (#11990)
adf9c3f 
Part of #9317.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kmill kmill kmill left review comments

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

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.

5 participants

@Parcly-Taxel @kmill @jcommelin @YaelDillies @fpvandoorn