Commit 2023-02-27 13:07 421d77e2

View on Github →

feat: Port Combinatorics.SimpleGraph.StronglyRegular (#2476)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.card_neighborFinset_eq_degree

Created Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

added theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl

added theorem SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl

added theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_eq

added theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj

added theorem SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj

added theorem SimpleGraph.IsSRGWith.compl

added theorem SimpleGraph.IsSRGWith.compl_is_regular

added theorem SimpleGraph.IsSRGWith.top

added structure SimpleGraph.IsSRGWith

added theorem SimpleGraph.bot_strongly_regular

added theorem SimpleGraph.compl_neighborFinset_sdiff_inter_eq

added theorem SimpleGraph.sdiff_compl_neighborFinset_inter_eq