This module defines the adjacency matrix of a graph, and provides theorems connecting graph properties to computational properties of the matrix.
adj_matrixis the adjacency matrix of a
simple_graphwith coefficients in a given semiring.
adj_matrix G R is the matrix
A such that
A i j = (1 : R) if
adjacent in the simple graph
G, and otherwise
A i j = 0.