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: Girth of a simple graph #6948

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: Girth of a simple graph #6948

wants to merge 8 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Sep 4, 2023 •
edited by github-actions bot

Define the girth of a simple graph as a ℕ∞.

This is not much API, but the goal is to be able to state the chromatic-girth theorem in case a LFTCM attendee wants to formalise it. cc @RemyDegenne

Open in Gitpod

@YaelDillies
feat: More complete lattice WithTop lemmas
b0ad7a8 
and corresponding lemmas for `ℕ∞`.

Also fix implicitness of `iff` lemmas.
@YaelDillies
fix
358342d
@YaelDillies
a few more lemmas
64d2890
@YaelDillies
fix Analysis.NormedSpace.OperatorNorm
5e05447
@YaelDillies
feat: Girth of a simple graph
a8b786d 
Define the girth of a simple graph as a `ℕ∞`.
@YaelDillies YaelDillies added blocked-by-other-PR This PR depends on another PR which is still in the queue. awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Sep 4, 2023
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 4, 2023
@bors bors bot changed the base branch from iInf_coe_eq_top to master September 4, 2023 14:40
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Sep 4, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 4, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Sep 4, 2023
bors bot pushed a commit that referenced this pull request Sep 4, 2023
@YaelDillies
feat: Girth of a simple graph (#6948)
02e140c 
Define the girth of a simple graph as a `ℕ∞`.
@bors
Copy link

bors bot commented Sep 4, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: Girth of a simple graph [Merged by Bors] - feat: Girth of a simple graph Sep 4, 2023
@bors bors bot closed this Sep 4, 2023
@bors bors bot deleted the girth branch September 4, 2023 20:45
ebab pushed a commit that referenced this pull request Sep 6, 2023
@YaelDillies @ebab
feat: Girth of a simple graph (#6948)
6fbc306 
Define the girth of a simple graph as a `ℕ∞`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill Awaiting requested review from kmill

Assignees
No one assigned
Labels
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.

None yet
3 participants
@YaelDillies @leanprover-community-mathlib4-bot @jcommelin