Theorems · Theorem · combinatorics

SimpleGraph.circulantGraph_adj

∀ {G : Type u_1} [inst : AddGroup G] (s : Set G) (a b : G),
  (SimpleGraph.circulantGraph s).Adj a b = (¬a = b ∧ (a - b ∈ s ∨ b - a ∈ s))

Defined in

Mathlib.Combinatorics.SimpleGraph.Circulant

Cited by

3 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

AddGroup