mathlib3

541688b5 - feat(combinatorics/simple_graph/basic): add lemmas about cardinality of common neighbor set (#5789)

feat(combinatorics/simple_graph/basic): add lemmas about cardinality of common neighbor set (#5789) Add lemmas about the cardinality of the set of common neighbors between two vertices. Add note in module docstring about naming convention. Part of #5698 in order to prove facts about strongly regular graphs. Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>