circulantGraph — Mathlib

English

The circulant graph on an additive group G with jumps s is the graph on G where x is adjacent to y if and only if x − y ∈ s.

Русский

Циркулярный граф над аддитивной группой G с прыжками s строится так, что вершины x и y смежны тогда и только тогда, когда x − y ∈ s.

LaTeX

$$(circulantGraph(s)).Adj x y ⇔ x - y ∈ s$$

Lean4

/-- Circulant graph over additive group `G` with jumps `s` -/
@[simps!]
def circulantGraph {G : Type*} [AddGroup G] (s : Set G) : SimpleGraph G :=
  fromRel (· - · ∈ s)

Похожие утверждения