mathlib documentation


Strongly regular graphs #

Main definitions #


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 : ) :

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

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.