Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 19:11 1107693b

View on Github →

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.

Estimated changes