Theorems · Theorem · combinatorics

SimpleGraph.adjMatrix_vecMul_apply

∀ {α : 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 → α),
  Matrix.vecMul vec (SimpleGraph.adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u

Defined in: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Cited by: 0 results in Mathlib
Foundations: Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableRel Fintype NonAssocSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Fintypestatement and proof · cited by 7,736
Finset.sumstatement · cited by 5,195
Matrixproof · cited by 4,303
SimpleGraphstatement and proof · cited by 3,072
SimpleGraph.Adjstatement and proof · cited by 1,346
NonAssocSemiringstatement and proof · cited by 805
SimpleGraph.neighborSetstatement · cited by 257
dotProductproof · cited by 194
Matrix.vecMulstatement · cited by 148
SimpleGraph.neighborFinsetstatement · cited by 72
SimpleGraph.adjMatrixstatement and proof · cited by 48

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.