Rida Hamadani issues

Results 4 issues of


                                            Rida Hamadani

feat(Combinatorics/SimpleGraph): Provide iff statements for distance equal and greater than 2

I need these lemmas to prove that Moore graphs of girth 5 are strongly regular. --- - [ ] depends on: #11945 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

awaiting-review

merge-conflict

t-combinatorics

feat(Combinatorics/SimpleGraph): Define diameter of simple graphs and provide basic lemmas related to it

This defines the diameter of a simple graph, and provides a basic API for it. Co-authored-by: Matt Diamond --- - [ ] depends on: #11945 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

awaiting-review

merge-conflict

t-combinatorics

feat(Combinatorics/SimpleGraph): vertices are not reachable iff set of walks between them is empty

This lemma came up while extending `SimpleGraph.dist` to `ENat`. Co-authored-by: Kyle Miller --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

awaiting-review

easy

t-combinatorics

Delimiters should go on their own line in multiline docs

Check [this](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/style.20guide.20for.20comments.3F) topic on Zulip.

style-guide