Theorems · Definition · combinatorics

Matrix.IsAdjMatrix.toGraph

{α : Type u_1} →
  {V : Type u_2} → {A : Matrix V V α} → [inst : MulZeroOneClass α] → [Nontrivial α] → A.IsAdjMatrix → SimpleGraph V

For A : Matrix V V α and h : IsAdjMatrix A, h.toGraph is the simple graph whose adjacency matrix is A.

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

9 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

MulZeroOneClassNontrivial