mathlib3

1107693b - feat(combinatorics/simple_graph/basic): add lemmas about the neighbor set of a vertex in the complement graph (#7138)

feat(combinatorics/simple_graph/basic): add lemmas about the neighbor set of a vertex in the complement graph (#7138) Add lemmas about the neighbor set of a vertex in the complement graph, including a lemma proving that the complement of a regular graph is regular. Part of #5698 in order to prove facts about strongly regular graphs. Co-authored-by: Kyle Miller <kmill31415@gmail.com>