Theorems · Theorem · combinatorics

SimpleGraph.IsSRGWith.matrix_eq

∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V] {α : Type u_1} [inst_3 : Semiring α],
  G.IsSRGWith n k ℓ μ →
    SimpleGraph.adjMatrix α G ^ 2 = k • 1 + ℓ • SimpleGraph.adjMatrix α G + μ • SimpleGraph.adjMatrix α Gᶜ

Let A and C be the adjacency matrices of a strongly regular graph with parameters n k ℓ μ and its complement respectively and I be the identity matrix, then A ^ 2 = k • I + ℓ • A + μ • C. C is equivalent to the expression J - I - A more often found in the literature, where J is the all-ones matrix.

Defined in

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRelDecidableEqSemiring