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 <067de2d7f4f5809454de1022e9c3aab9efe72888@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib