Skip to content

feat(Combinatorics/SimpleGraph): Cayley graph for structures with Mul/Add#35084

Open
edegeltje wants to merge 23 commits intoleanprover-community:masterfrom
edegeltje:cayley_graph
Open

feat(Combinatorics/SimpleGraph): Cayley graph for structures with Mul/Add#35084
edegeltje wants to merge 23 commits intoleanprover-community:masterfrom
edegeltje:cayley_graph

Conversation

@edegeltje
Copy link
Copy Markdown
Collaborator

@edegeltje edegeltje commented Feb 10, 2026 •
edited
Loading

This pr:

  • adds the definition SimpleGraph.mulCayley, where x is adjacent to a distinct y when there is g such that x * g = y or x = y * g,
  • proves various lemmas about the above,
  • adds/proves the additive versions of all of the above

some related zulip conversation: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cayley.20and.20circulant.20graph/with/572839048

Open in Gitpod

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

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

PR summary 2352820370

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.SimpleGraph.Cayley (new file) 534

Declarations diff

+ instance [DecidableEq M] [DecidablePred (· ∈ s)] : DecidableRel (mulCayley s).Adj
+ instance [Fintype M] [DecidableEq M] [DecidablePred (· ∈ s)] :
+ mulCayley
+ mulCayley_adj
+ mulCayley_adj'
+ mulCayley_adj_mul_iff_right
+ mulCayley_compl_singleton_one
+ mulCayley_empty
+ mulCayley_erase_one
+ mulCayley_gc
+ mulCayley_insert_one
+ mulCayley_inv
+ mulCayley_le_iff
+ mulCayley_mono
+ mulCayley_singleton_one
+ mulCayley_union
+ mulCayley_univ

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.

Increase in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
8701 2 backward.isDefEq

Current commit 1b6a2c1468
Reference commit 2352820370

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

vihdzp
vihdzp reviewed Feb 10, 2026
View reviewed changes
@edegeltje edegeltje requested a review from vihdzp February 11, 2026 16:53
vlad902
vlad902 reviewed Feb 11, 2026
View reviewed changes
vlad902
vlad902 reviewed Feb 11, 2026
View reviewed changes
vlad902 added a commit to vlad902/mathlib4 that referenced this pull request Feb 13, 2026
@vlad902
feat(SimpleGraph): redefine cycleGraph independent of circulanGraph
e0c3a44 
Right now the `cycleGraph` definition relies on `circulantGraph` which
requires importing Group definitions from the algebra hierarchy. This
causes large-imports for me in later PRs where I try to make more
widespread use of cycleGraphs, so here I redefine it to be its own
independent object, and leave splitting it from `circulantGraph` to
another PR (this is parallel to leanprover-community#35084.)
@vlad902 vlad902 mentioned this pull request Feb 13, 2026
Open
SnirBroshi
SnirBroshi reviewed Feb 13, 2026
View reviewed changes
vlad902 added a commit to vlad902/mathlib4 that referenced this pull request Feb 13, 2026
@vlad902
feat(SimpleGraph): redefine cycleGraph independent of circulanGraph
36a2763 
Right now the `cycleGraph` definition relies on `circulantGraph` which
requires importing Group definitions from the algebra hierarchy. This
causes large-imports for me in later PRs where I try to make more
widespread use of cycleGraphs, so here I redefine it to be its own
independent object, and leave splitting it from `circulantGraph` to
another PR (this is parallel to leanprover-community#35084.)
SnirBroshi
SnirBroshi reviewed Feb 24, 2026
View reviewed changes
SnirBroshi
SnirBroshi reviewed Feb 24, 2026
View reviewed changes
@YaelDillies YaelDillies changed the title feat(Combinatorics/SimpleGraph): The Cayley graph for structures with Mul/Add feat(Combinatorics/SimpleGraph): Cayley graph for structures with Mul/Add Mar 16, 2026
YaelDillies
YaelDillies reviewed Mar 16, 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.

Could you sort the lemmas into Mul, MulOneClass, Group sections?

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 16, 2026
YaelDillies
YaelDillies reviewed Mar 17, 2026
View reviewed changes
@edegeltje edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
vihdzp
vihdzp reviewed Mar 18, 2026
View reviewed changes
YaelDillies
YaelDillies reviewed Mar 18, 2026
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
@edegeltje edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
YaelDillies
YaelDillies reviewed Mar 18, 2026
View reviewed changes
YaelDillies
YaelDillies reviewed Mar 18, 2026
View reviewed changes
YaelDillies
YaelDillies reviewed Mar 18, 2026
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
@edegeltje edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 18, 2026
YaelDillies
YaelDillies approved these changes Mar 19, 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

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 19, 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 19, 2026
@YaelDillies YaelDillies removed their assignment Mar 19, 2026
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026
@edegeltje edegeltje removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026
vlad902
vlad902 reviewed Mar 24, 2026
View reviewed changes
vlad902
vlad902 reviewed Mar 24, 2026
View reviewed changes
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

+3 more reviewers

@vlad902 vlad902 vlad902 left review comments

@SnirBroshi SnirBroshi SnirBroshi left review comments

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@kmill kmill

@awainverse awainverse

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@edegeltje @vlad902 @YaelDillies @SnirBroshi @vihdzp @kmill @jcommelin @awainverse