Documentation

Mathlib.Combinatorics.SimpleGraph.Circulant

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 #

@[simp]
theorem SimpleGraph.circulantGraph_adj {G : Type u_1} [AddGroup G] (s : Set G) (a : G) (b : G) :
(SimpleGraph.circulantGraph s).Adj a b = (¬a = b (a - b s b - a s))

Circulant graph over additive group G with jumps s

Equations
Instances For
    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 : G} {v : G} {d : G} :
    theorem SimpleGraph.cycleGraph_adj {n : } {u : Fin (n + 2)} {v : Fin (n + 2)} :
    (SimpleGraph.cycleGraph (n + 2)).Adj u v u - v = 1 v - u = 1
    theorem SimpleGraph.cycleGraph_adj' {n : } {u : Fin n} {v : Fin n} :
    (SimpleGraph.cycleGraph n).Adj u v (u - v) = 1 (v - u) = 1
    theorem SimpleGraph.cycleGraph_neighborSet {n : } {v : Fin (n + 2)} :
    (SimpleGraph.cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}
    theorem SimpleGraph.cycleGraph_neighborFinset {n : } {v : Fin (n + 2)} :
    (SimpleGraph.cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}
    theorem SimpleGraph.cycleGraph_degree_two_le {n : } {v : Fin (n + 2)} :
    (SimpleGraph.cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card
    theorem SimpleGraph.cycleGraph_degree_three_le {n : } {v : Fin (n + 3)} :
    (SimpleGraph.cycleGraph (n + 3)).degree v = 2