Theorems · Theorem · combinatorics

SimpleGraph.adjMatrix_dotProduct

∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  SimpleGraph.adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableRelFintypeNonAssocSemiring