Theorems · Theorem · combinatorics

SimpleGraph.IsSRGWith.param_eq

∀ {n k ℓ μ : ℕ} {V : Type u} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],
  G.IsSRGWith n k ℓ μ → 0 < n → k * (k - ℓ - 1) = (n - k - 1) * μ

The parameters of a strongly regular graph with at least one vertex satisfy k * (k - ℓ - 1) = (n - k - 1) * μ.

Defined in

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRel