Theorems · Theorem · combinatorics

SimpleGraph.diagonal_hadamard_adjMatrix

∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] (d : V → α), (Matrix.diagonal d).hadamard (SimpleGraph.adjMatrix α G) = 0

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableRelDecidableEqMulZeroOneClass