feat(Combinatorics/SimpleGraph): If a graph has a Walk starting and ending in the same vertex then the chromatic number is grater than two

[IvanRenison]

---

The theorem is named Walk.two_lt_chromaticNumber_of_odd_closed, but I'm not sure if that is the best name. I didn't use the word cycle because in Connectivity.lean a cycle is defined as a Walk that start and ends in the same vertex and has no other repeated vertex, so it's not what I'm using here.

[github-actions[bot]]

PR summary e7dc15037a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.ConcreteColorings	617	619	+2 (+0.32%)

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.ConcreteColorings	2

---

Declarations diff

+ Walk.three_le_chromaticNumber_of_odd_loop

You can run this locally as follows

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

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

[kmill]

Thanks!

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style