Commit 2022-01-01 00:20 da54388a

View on Github →

feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements (#5698) We add the definition of a strongly regular graph and prove some useful lemmas about them.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.bot_degree

added theorem simple_graph.card_common_neighbors_top

added theorem simple_graph.common_neighbors_top_eq

deleted theorem simple_graph.complete_graph_is_regular

deleted theorem simple_graph.is_regular_compl_of_is_regular

added theorem simple_graph.is_regular_of_degree.compl

added theorem simple_graph.is_regular_of_degree.degree_eq

added theorem simple_graph.is_regular_of_degree.top

deleted theorem simple_graph.is_regular_of_degree_eq

added theorem simple_graph.ne_of_adj_of_not_adj

added theorem simple_graph.neighbor_finset_compl

added theorem simple_graph.neighbor_finset_def

Modified src/combinatorics/simple_graph/strongly_regular.lean

added theorem simple_graph.bot_strongly_regular

added theorem simple_graph.compl_neighbor_finset_sdiff_inter_eq

deleted theorem simple_graph.complete_strongly_regular

deleted structure simple_graph.is_SRG_of

added theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_adj_compl

added theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_not_adj_compl

added theorem simple_graph.is_SRG_with.card_neighbor_finset_union_eq

added theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_adj

added theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_not_adj

added theorem simple_graph.is_SRG_with.compl

added theorem simple_graph.is_SRG_with.compl_is_regular

added theorem simple_graph.is_SRG_with.top

added structure simple_graph.is_SRG_with

added theorem simple_graph.sdiff_compl_neighbor_finset_inter_eq

Modified src/data/fintype/basic.lean

added theorem finset.compl_inter

added theorem finset.compl_union

added theorem finset.inter_compl

modified theorem finset.union_compl

Modified src/data/set/finite.lean

added theorem set.to_finset_sdiff

added theorem set.to_finset_singleton

Modified src/measure_theory/measure/outer_measure.lean