Theorems · Theorem · combinatorics

SimpleGraph.lapMatrix_mulVec_apply

∀ {V : Type u_1} {R : Type u_2} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocRing R] (v : V) (vec : V → R),
  (SimpleGraph.lapMatrix R G).mulVec vec v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u

Defined in

Mathlib.Combinatorics.SimpleGraph.LapMatrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRelDecidableEqNonAssocRing