Theorems · Definition · combinatorics

SimpleGraph.adjMatrix

(α : Type u_1) → {V : Type u_2} → (G : SimpleGraph V) → [DecidableRel G.Adj] → [Zero α] → [One α] → Matrix V V α

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

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

48 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

DecidableRelZeroOne