# mathlibdocumentation

This module defines the adjacency matrix of a graph, and provides theorems connecting graph properties to computational properties of the matrix.

## Main definitions

• adj_matrix is the adjacency matrix of a simple_graph with coefficients in a given semiring.
def simple_graph.adj_matrix {α : Type u} [fintype α] (R : Type v) [semiring R] (G : simple_graph α) [decidable_rel G.adj] :
α R

adj_matrix G R is the matrix A such that A i j = (1 : R) if i and j are adjacent in the simple graph G, and otherwise A i j = 0.

Equations
@[simp]
theorem simple_graph.adj_matrix_apply {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (v w : α) :
w = ite (G.adj v w) 1 0

@[simp]
theorem simple_graph.transpose_adj_matrix {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] :

@[simp]
theorem simple_graph.adj_matrix_dot_product {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (v : α) (vec : α → R) :
vec = ∑ (u : α) in , vec u

@[simp]
theorem simple_graph.dot_product_adj_matrix {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (v : α) (vec : α → R) :
v) = ∑ (u : α) in , vec u

@[simp]
theorem simple_graph.adj_matrix_mul_vec_apply {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (v : α) (vec : α → R) :
vec v = ∑ (u : α) in , vec u

@[simp]
theorem simple_graph.adj_matrix_vec_mul_apply {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (v : α) (vec : α → R) :
v = ∑ (u : α) in , vec u

@[simp]
theorem simple_graph.adj_matrix_mul_apply {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (M : α R) (v w : α) :
M) v w = ∑ (u : α) in , M u w

@[simp]
theorem simple_graph.mul_adj_matrix_apply {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (M : α R) (v w : α) :
(M v w = ∑ (u : α) in , M v u

theorem simple_graph.trace_adj_matrix {α : Type u} [fintype α] (R : Type v) [semiring R] (G : simple_graph α) [decidable_rel G.adj] :
R R) = 0

theorem simple_graph.adj_matrix_mul_self_apply_self {α : Type u} [fintype α] {R : Type v} [semiring R] (G : simple_graph α) [decidable_rel G.adj] (i : α) :
i i = (G.degree i)

@[simp]
theorem simple_graph.adj_matrix_mul_vec_const_apply {α : Type u} [fintype α] {R : Type v} [semiring R] {G : simple_graph α} [decidable_rel G.adj] {r : R} {v : α} :
r) v = ((G.degree v)) * r

theorem simple_graph.adj_matrix_mul_vec_const_apply_of_regular {α : Type u} [fintype α] {R : Type v} [semiring R] {G : simple_graph α} [decidable_rel G.adj] {d : } {r : R} (hd : G.is_regular_of_degree d) {v : α} :
r) v = (d) * r