Commit 2021-01-13 18:52 0b9fbc48

View on Github →

feat(combinatorics/simple_graph/basic): add definition of common neighbors and lemmas (#5718) Part of #5698 in order to prove facts about strongly regular graphs

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added def simple_graph.common_neighbors

added theorem simple_graph.common_neighbors_eq

added theorem simple_graph.common_neighbors_subset_neighbor_set

added theorem simple_graph.common_neighbors_symm

added theorem simple_graph.degree_lt_card_verts

added theorem simple_graph.is_regular_of_degree_eq

added theorem simple_graph.not_mem_common_neighbors_left

added theorem simple_graph.not_mem_common_neighbors_right