adjMatrix_dotProduct — Mathlib

English

The dot product of the adjacency matrix with a vector equals the sum over the neighbor set.

Русский

Один из способов вычисления скалярного произведения с матрицей смежности — сумма значений соседей.

LaTeX

$$dotProduct(G.adjMatrix α G v, vec) = (G.neighborFinset v).sum (fun u => vec u)$$

Lean4

@[simp]
theorem adjMatrix_dotProduct [NonAssocSemiring α] (v : V) (vec : V → α) :
    G.adjMatrix α v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u := by
  simp [neighborFinset_eq_filter, dotProduct, sum_filter]

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