adjMatrix_mulVec_apply — Mathlib

English

Left multiplication of a vector by the adjacency matrix yields the neighbor-sum vector.

Русский

Левое умножение матрицы смежности на вектор даёт сумму значений соседей.

LaTeX

$$$(G.adjMatrix α * vec) v = \\sum_{u \\in \\mathrm{neighborFinset}(G,v)} vec(u)$$

Lean4

@[simp]
theorem adjMatrix_mulVec_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
    (G.adjMatrix α *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u := by rw [mulVec, adjMatrix_dotProduct]

Похожие утверждения