Definition of circulant graphs #
This file defines and proves several fact about circulant graphs.
A circulant graph over type G
with jumps s : Set G
is a graph in which two vertices u
and v
are adjacent if and only if u - v ∈ s
or v - u ∈ s
. The elements of s
are called jumps.
Main declarations #
SimpleGraph.circulantGraph s
: the circulant graph overG
with jumpss
.SimpleGraph.cycleGraph n
: the cycle graph overFin n
.
Circulant graph over additive group G
with jumps s
Equations
- SimpleGraph.circulantGraph s = SimpleGraph.fromRel fun (x1 x2 : G) => x1 - x2 ∈ s
Instances For
instance
SimpleGraph.instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet
{G : Type u_1}
[AddGroup G]
(s : Set G)
[DecidableEq G]
[DecidablePred fun (x : G) => x ∈ s]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
SimpleGraph.circulantGraph_adj_translate
{G : Type u_1}
[AddGroup G]
{s : Set G}
{u v d : G}
: