mathlib3

da54388a - feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements (#5698)

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. Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>