Theorems · Theorem · combinatorics

Matrix.IsAdjMatrix.toGraph_compl_eq

∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] {A : Matrix V V α}
  [inst_2 : MulZeroOneClass α] [inst_3 : Nontrivial α] (h : A.IsAdjMatrix), ⋯.toGraph = h.toGraphᶜ

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqMulZeroOneClassNontrivial