[Merged by Bors] - chore: move 300 lines off Combinatorics/SimpleGraph/Connectivity

[grunweg]

Move material about walks as subgraphs and walk-counting to separate files.

Mostly import-directed; I'm not a graph theorist - please comment if this split doesn't make sense!

---

(Also, feel free to suggest if the new module docstring should be extended!)

[github-actions]

PR summary 29dcdf82d7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
4 files Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Matching	1
Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting	520

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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>

[YaelDillies]

@adomani surely the import summary is wrong? This PR is supposed to significantly change imports

[adomani]

I wonder whether this is another situation where using "number of transitive imports" is not really the metric that we should be using. In this PR, as far as I understand, you

• added a new leaf and
• replaced a few edges into the file from which you extracted the new leaf to point to the new leaf.

The import changes does tell you that

• the new leaf WalkCounting now has 515 transitive imports (it did not exist earlier, so far so good);
• AdjMatrix and the files that import it gained one transitive import, since they now point to the new leaf on their way to then having the same imports.

In conclusion, I think that the import tool is working as it was programmed to work. I still agree that this is probably not the measure that we should necessarily look at to make import-based decisions.

[adomani]

I feel that a more reasonable measure would be to find the number of covering relations among imports, or maybe the average number of covering relations per vertex.

[kim-em]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mattrobball]

bors r-

[mathlib-bors]

Canceled.

[mattrobball]

Unclosed section.

bors delegate+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

CI is virtually green (only environment linting remains, which this PR didn't touch), so
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style