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

[edegeltje]

This pr:

• adds the definition SimpleGraph.mulCayley, defining the simple graph induced by a Mul instance,
• proves various lemmas about the above,
• adds/proves the additive versions of all of the above,
• redefines SimpleGraph.circulantGraph to use addCayley,
• reproves lemmas about circulantGraph to use the new addCayley lemmas.

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

---

[github-actions]

PR summary d1366e1a1a

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

---

Declarations diff

+ instance [Group G] [DecidableEq G] [DecidablePred (· ∈ s)] : DecidableRel (mulCayley s).Adj
+ instance [Mul G] [Fintype G] [DecidableEq G] [DecidablePred (· ∈ s)] :
+ mulCayley
+ mulCayley_adj
+ mulCayley_adj'
+ mulCayley_adj_mul_left_iff
+ mulCayley_compl_singleton_one
+ mulCayley_empty
+ mulCayley_eq_erase_one
+ mulCayley_eq_symm
+ mulCayley_eq_union_one
+ mulCayley_mono
+ mulCayley_singleton_one
+ mulCayley_univ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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]

Does unfold mulCayley; grind or unfold mulCayley; aesop work?

[edegeltje]

yes, the aesop version works... but i prefer not to use hammers. Is it ok that i changed it to a one-liner using simp instead?