Skip to content

feat(Combinatorics/SimpleGraph/Walk): chords of walks#35906

Open
scp020 wants to merge 54 commits intoleanprover-community:masterfrom
scp020:master
Open

feat(Combinatorics/SimpleGraph/Walk): chords of walks#35906
scp020 wants to merge 54 commits intoleanprover-community:masterfrom
scp020:master

Conversation

@scp020
Copy link
Copy Markdown

@scp020 scp020 commented Mar 1, 2026 •
edited
Loading

Define Walk.IsChord and Walk.IsChordless predicates in a new file SimpleGraph/Walks/Chord.lean.

See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory

Zulip

Open in Gitpod

@github-actions 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 Mar 1, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 1, 2026

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.

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
Copy link
Copy Markdown

github-actions bot commented Mar 1, 2026 •
edited
Loading

PR summary 54d69dfd22

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.SimpleGraph.Walk.Chord (new file) 546

Declarations diff

+ IsChord
+ IsChordless
+ IsChordless.mem_edges
+ isChord_sym2Mk
+ isChordless_iff_forall_mem_edges

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).

@github-actions github-actions bot added the t-combinatorics Combinatorics label Mar 1, 2026
@scp020 scp020 changed the title Add SimpleGraph.Walk.IsChord and SimpleGraph.Walk.IsChordless feat(Combinatorics/SimpleGraph/Walks): add Walk.IsChord and Walk.IsChordless Mar 1, 2026
@scp020 scp020 marked this pull request as ready for review March 2, 2026 11:35
@github-actions github-actions bot added easy < 20s of review time. See the lifecycle page for guidelines. CI Modifies the continuous integration setup or other automation and removed easy < 20s of review time. See the lifecycle page for guidelines. CI Modifies the continuous integration setup or other automation labels Mar 2, 2026
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Mar 4, 2026
View reviewed changes
@scp020 scp020 requested a review from YaelDillies March 26, 2026 00:54
@scp020
Copy link
Copy Markdown
Author

scp020 commented Mar 26, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 26, 2026
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 26, 2026
@scp020
Copy link
Copy Markdown
Author

scp020 commented Mar 27, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Apr 1, 2026

This pull request has conflicts, please merge master and resolve them.

@YaelDillies YaelDillies changed the title feat(Combinatorics/SimpleGraph/Walks): chords of walks feat(Combinatorics/SimpleGraph/Walk): chords of walks Apr 3, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 4, 2026
SnirBroshi
SnirBroshi reviewed Apr 4, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@SnirBroshi SnirBroshi left a comment

Choose a reason for hiding this comment

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

Thanks!

scp020 and others added 11 commits April 5, 2026 09:00
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
20486e4 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
e358ae0 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
e3b3ef0 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
4091093 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
4938b4d 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
e4daeff 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
cec9b20 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
3a56880 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
c15a16f 
Co-authored-by: Snir Broshi <[email protected]>
@scp020 @SnirBroshi
Update Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean
62df181 
Co-authored-by: Snir Broshi <[email protected]>
@scp020
Merge branch 'leanprover-community:master' into master
45c2545
@scp020
Copy link
Copy Markdown
Author

scp020 commented Apr 5, 2026

Thanks!

Thank you for catching the errors I had overlooked; your corrections were extremely thorough.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies Awaiting requested review from YaelDillies

1 more reviewer

@SnirBroshi SnirBroshi SnirBroshi left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@YaelDillies YaelDillies

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@scp020 @YaelDillies @SnirBroshi