# mathlibdocumentation

combinatorics.simple_graph.strongly_regular

# Strongly regular graphs #

## Main definitions #

• G.is_SRG_of n k l m (see is_simple_graph.is_SRG_of) is a structure for a simple_graph satisfying the following conditions:
• The cardinality of the vertex set is n
• G is a regular graph with degree k
• The number of common neighbors between any two adjacent vertices in G is l
• The number of common neighbors between any two nonadjacent vertices in G is m

## TODO #

• Prove that the complement of a strongly regular graph is strongly regular with parameters is_SRG_of n (n - k - 1) (n - 2 - 2k + m) (v - 2k + l)
• Prove that the parameters of a strongly regular graph obey the relation (n - k - 1) * m = k * (k - l - 1)
• Prove that if I is the identity matrix and J is the all-one matrix, then the adj matrix A of SRG obeys relation A^2 = kI + lA + m(J - I - A)
structure simple_graph.is_SRG_of {V : Type u} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [decidable_eq V] (n k l m : ) :
Prop

A graph is strongly regular with parameters n k l m if

• its vertex set has cardinality n
• it is regular with degree k
• every pair of adjacent vertices has l common neighbors
• every pair of nonadjacent vertices has m common neighbors
theorem simple_graph.complete_strongly_regular {V : Type u} [fintype V] [decidable_eq V] (m : ) :
(fintype.card V) - 1) - 2) m

Complete graphs are strongly regular. Note that the parameter m can take any value for complete graphs, since there are no distinct pairs of nonadjacent vertices.