Theorems · Theorem · combinatorics

SimpleGraph.mul_adjMatrix_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),
  (M * SimpleGraph.adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v 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: 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
mul_oneproof · cited by 3,885
Finset.univproof · cited by 3,473
SimpleGraphstatement and proof · cited by 3,072
Finset.sum_congrproof · cited by 2,323
MulZeroClass.mul_zeroproof · cited by 2,091
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_mul_self_apply_selfproof · cited by 0