feat(Combinatorics/SimpleGraph/StarGraph): define star graphs by 8e7 · Pull Request #38027 · leanprover-community/mathlib4

8e7 · 2026-04-14T03:43:28Z

Add a new definition starGraph and several key lemmas. Star graphs are a trivial class of tree, often used in constructive proofs regarding trees.

All lemmas are hand written first, then golfed with the help of Claude Code.

github-actions · 2026-04-14T03:43:42Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-04-14T03:44:32Z

PR summary 8e3c989104

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.StarGraph` (new file)	978

Declarations diff

+ connected_starGraph
+ degree_starGraph_center
+ degree_starGraph_of_ne_center
+ instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj
+ isAcyclic_starGraph
+ isTree_starGraph
+ starGraph
+ starGraph_adj
+ starGraph_center_adj
+ starGraph_center_adj'

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 · 2026-04-14T07:27:56Z

Please mark the review comments 'resolved' once you've addressed them so the next reviewer doesn't think they're still open.

Co-authored-by: Vlad Tsyrklevich <vlad902@gmail.com>

IvanRenison

I like the idea!
Maybe we should have StarGraph in a separate graph

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com>

SnirBroshi · 2026-04-15T17:21:45Z

I think Star.lean would be a better name based on this (to not repeat "Graph"), but I'm not sure.

(unless we want to define a Star (SimpleGraph V) operation, but I don't think we do)

I think starGraph is better since star is already in Mathlib/Algebra/Notation, and other specific types of graphs have the -graph suffix, such as lineGraph and pathGraph.

8e7 added 2 commits April 14, 2026 10:30

feat(Combinatorics/SimpleGraph/Acyclic): add star graph

34ca34e

Fixing docstrings

e672972

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 Apr 14, 2026

github-actions bot added the t-combinatorics Combinatorics label Apr 14, 2026

Merge branch 'master' into star_graph

9f9e7c7

vlad902 reviewed Apr 14, 2026

View reviewed changes

8e7 added 2 commits April 14, 2026 14:55

Golf proofs and set lemmas to public.

cfa0439

Merge branch 'star_graph' of github.com:8e7/mathlib4 into star_graph

d1a36c9

vlad902 reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

vihdzp reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

8e7 and others added 3 commits April 14, 2026 15:37

Update Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

eebb8e1

Co-authored-by: Vlad Tsyrklevich <vlad902@gmail.com>

Fix lemma naming

d3c0233

Merge branch 'star_graph' of github.com:8e7/mathlib4 into star_graph

3a1e62f

IvanRenison suggested changes Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

SnirBroshi reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

8e7 and others added 4 commits April 15, 2026 10:16

Apply suggestion from @SnirBroshi

18da22a

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Apply suggestions from code review

4312997

Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com>

minor change: use inferInstanceAs, add symmetric starGraph_center_adj'

76e69e1

refactor to StarGraph.lean

c1ee37d

8e7 changed the title ~~feat(Combinatorics/SimpleGraph/Acyclic): define star graphs~~ feat(Combinatorics/SimpleGraph/StarGraph): define star graphs Apr 15, 2026

vlad902 reviewed Apr 15, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/StarGraph.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/StarGraph.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/StarGraph.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/StarGraph.lean Outdated

SnirBroshi reviewed Apr 15, 2026

View reviewed changes

8e7 and others added 2 commits April 16, 2026 11:11

apply reviewer suggestions

4395c70

Merge branch 'master' into star_graph

38aa9f1

8e7 requested a review from JovanGerb April 16, 2026 09:13

Conversation

8e7 commented Apr 14, 2026

Uh oh!

github-actions bot commented Apr 14, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8e3c989104

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vlad902 commented Apr 14, 2026

Uh oh!

Uh oh!

IvanRenison left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

8e7 Apr 16, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Apr 14, 2026 •

edited

Loading

SnirBroshi Apr 15, 2026 •

edited

Loading