Theorems · Theorem · combinatorics

SimpleGraph.adjMatrix_mulVec_const_apply

∀ {α : Type u_1} {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] {a : α} {v : V},
  (SimpleGraph.adjMatrix α G).mulVec (Function.const V a) v = ↑(G.degree v) * a

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.

Cites12

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
SimpleGraphstatement and proof · cited by 3,072
SimpleGraph.Adjstatement and proof · cited by 1,346
NonAssocSemiringstatement and proof · cited by 805
nsmul_eq_mulproof · cited by 369
Matrix.mulVecstatement · cited by 267
SimpleGraph.neighborSetstatement · cited by 257
Finset.sum_constproof · cited by 254
SimpleGraph.degreestatement and proof · cited by 112
SimpleGraph.adjMatrixstatement · cited by 48
SimpleGraph.adjMatrix_mulVec_applyproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.