Strongly regular graphs #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
G.is_SRG_with n k ℓ μ (see
simple_graph.is_SRG_with) is a structure for
simple_graph satisfying the following conditions:
- The cardinality of the vertex set is
G is a regular graph with degree
- The number of common neighbors between any two adjacent vertices in
- The number of common neighbors between any two nonadjacent vertices in
- Prove that the parameters of a strongly regular graph
obey the relation
(n - k - 1) * μ = k * (k - ℓ - 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 + ℓA + μ(J - I - A)
A graph is strongly regular with parameters
n k ℓ μ if
- its vertex set has cardinality
- it is regular with degree
- every pair of adjacent vertices has
ℓ common neighbors
- every pair of nonadjacent vertices has
μ common neighbors
Empty graphs are strongly regular. Note that
ℓ can take any value
for empty graphs, since there are no pairs of adjacent vertices.
Complete graphs are strongly regular. Note that
μ can take any value
for complete graphs, since there are no distinct pairs of non-adjacent vertices.
G is strongly regular,
2*(k + 1) - m in
G is the number of vertices that are
adjacent to either
¬G.adj v w. So it's the cardinality of
G.neighbor_set v ∪ G.neighbor_set w.
The complement of a strongly regular graph is strongly regular.