Skip to content

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot#35627

Closed
SnirBroshi wants to merge 5 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/degree-top-bot
Closed

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot#35627
SnirBroshi wants to merge 5 commits intoleanprover-community:masterfrom
SnirBroshi:feature/simple-graph/degree-top-bot

Conversation

@SnirBroshi
Copy link
Copy Markdown
Collaborator

@SnirBroshi SnirBroshi commented Feb 22, 2026 •
edited
Loading

And a couple of lemmas about IsRegularOfDegree, e.g. the empty graph is regular of any degree.

Open in Gitpod

@github-actions github-actions bot added the t-combinatorics Combinatorics label Feb 22, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 22, 2026 •
edited
Loading

PR summary de4f458186

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsRegularOfDegree.bot
+ IsRegularOfDegree.maxDegree_eq
+ IsRegularOfDegree.minDegree_eq
+ IsRegularOfDegree.of_isEmpty
+ maxDegree_top
+ minDegree_top

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

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

vlad902
vlad902 approved these changes Feb 24, 2026
View reviewed changes
Comment thread Mathlib/Combinatorics/SimpleGraph/Finite.lean
· obtain ⟨_, hv⟩ := G.exists_maximal_degree_vertex
exact hv ▸ h _

theorem IsRegularOfDegree.maxDegree_eq [Nonempty V] [DecidableRel G.Adj] {d : ℕ}
Copy link
Copy Markdown
Collaborator

@vlad902 vlad902 Feb 24, 2026

Choose a reason for hiding this comment

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

I was going to suggest eliminating Nonempty V here, and then I realized G is regular of all degrees for IsEmpty V, gross.

Copy link
Copy Markdown
Collaborator

@vlad902 vlad902 Feb 24, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

Just had the thought that really what you're proving shows the correct definition, G.maxDegree = G.minDegree thought this has the unfortunate side effect of not working with locally finite graphs of unbounded degree (e.g. the type class assumption G.LocallyFinite would have to be weakened to Fintype V in the definition of IsRegularOfDegree.)

Copy link
Copy Markdown
Collaborator Author

@SnirBroshi SnirBroshi Feb 24, 2026

Choose a reason for hiding this comment

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

Yes, but unfortunately my #33501 hasn't gathered support. I'd love to avoid Fintype everywhere in the degree API.

Copy link
Copy Markdown
Collaborator

@vlad902 vlad902 Feb 24, 2026

Choose a reason for hiding this comment

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

The objection in that review seems to be to changing degree to work for infinite graphs, but if I understand correctly the objection was not to either 1) changing Fintype to Finite and 2) or defining edegree and friends. So we could still have maxEDegree/minEDegree for this definition.

Copy link
Copy Markdown
Collaborator Author

@SnirBroshi SnirBroshi Feb 24, 2026

Choose a reason for hiding this comment

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

Bhavik did object to (1), but (2) is still on the table. I'm planning to do (2).

YaelDillies
YaelDillies approved these changes Mar 18, 2026
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 delegate

Comment thread Mathlib/Combinatorics/SimpleGraph/Finite.lean
Comment thread Mathlib/Combinatorics/SimpleGraph/Finite.lean
Comment thread Mathlib/Combinatorics/SimpleGraph/Finite.lean
Comment thread Mathlib/Combinatorics/SimpleGraph/Finite.lean
@YaelDillies YaelDillies removed their assignment Mar 18, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 18, 2026

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

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 18, 2026
@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 19, 2026
@jcommelin jcommelin removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 21, 2026
@SnirBroshi SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 22, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator Author

SnirBroshi commented Mar 22, 2026

@jcommelin Hey, can you clarify why this is no longer considered maintainer merged?

@SnirBroshi SnirBroshi requested a review from YaelDillies March 23, 2026 04:27
YaelDillies
YaelDillies approved these changes Mar 23, 2026
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 Mar 23, 2026

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

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 23, 2026
b-mehta
b-mehta reviewed Apr 8, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta 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

mathlib-bors bot pushed a commit that referenced this pull request Apr 8, 2026
@SnirBroshi
feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot (#…
b6c608e 
…35627)

And a couple of lemmas about `IsRegularOfDegree`, e.g. the empty graph is regular of any degree.
@mathlib-triage mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 8, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 8, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot [Merged by Bors] - feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot Apr 8, 2026
@mathlib-bors mathlib-bors bot closed this Apr 8, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 10, 2026
@SnirBroshi @xroblot
feat(Combinatorics/SimpleGraph/Finite): min/max degrees of top/bot (l…
86d0209 
…eanprover-community#35627)

And a couple of lemmas about `IsRegularOfDegree`, e.g. the empty graph is regular of any degree.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@vlad902 vlad902 vlad902 approved these changes

Reviewers whose approvals may not affect merge requirements

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.

6 participants

@SnirBroshi @vlad902 @YaelDillies @b-mehta @kmill @jcommelin