Theorems · Theorem · combinatorics

SimpleGraph.adjMatrix_mul_apply

∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (M : Matrix V V α) (v w : V),
  (SimpleGraph.adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w

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: DecidableRel Fintype NonAssocSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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

Setstatement · cited by 53,352
AddCommMonoidproof · cited by 12,281
Fintypestatement and proof · cited by 7,736
Finset.sumstatement and proof · cited by 5,195
Matrixstatement and proof · cited by 4,303
Finset.univproof · cited by 3,473
SimpleGraphstatement and proof · cited by 3,072
one_mulproof · cited by 2,841
Finset.sum_congrproof · cited by 2,323
MulZeroClass.zero_mulproof · cited by 1,625
SimpleGraph.Adjstatement and proof · cited by 1,346
Finset.filterproof · cited by 949

Cited by1

Results whose statement or proof uses this declaration.

SimpleGraph.adjMatrix_pow_apply_eq_card_walkproof · cited by 1