mathlib documentation

combinatorics.simple_graph.adj_matrix

Adjacency Matrices #

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

Main definitions #

def simple_graph.adj_matrix {α : Type u} [fintype α] (R : Type v) [semiring R] (G : simple_graph α) [decidable_rel G.adj] :
matrix α α 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 : α) :
simple_graph.adj_matrix R G v w = ite (G.adj v w) 1 0
@[simp]
@[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) :
matrix.dot_product (simple_graph.adj_matrix R G v) vec = ∑ (u : α) in G.neighbor_finset v, 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) :
matrix.dot_product vec (simple_graph.adj_matrix R G v) = ∑ (u : α) in G.neighbor_finset v, 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) :
(simple_graph.adj_matrix R G).mul_vec vec v = ∑ (u : α) in G.neighbor_finset v, 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) :
matrix.vec_mul vec (simple_graph.adj_matrix R G) v = ∑ (u : α) in G.neighbor_finset v, 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 : matrix α α R) (v w : α) :
(simple_graph.adj_matrix R G M) v w = ∑ (u : α) in G.neighbor_finset v, 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 : matrix α α R) (v w : α) :
(M simple_graph.adj_matrix R G) v w = ∑ (u : α) in G.neighbor_finset w, M v u
theorem simple_graph.trace_adj_matrix {α : Type u} [fintype α] (R : Type v) [semiring R] (G : simple_graph α) [decidable_rel G.adj] :
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 : α) :
@[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 : α} :
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 : α} :