Theorems · Theorem · combinatorics

SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl

∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V],
  G.IsSRGWith n k ℓ μ → ∀ {v w : V}, Gᶜ.Adj v w → Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Defined in

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRelDecidableEq