dotProduct_adjMatrix — Mathlib

English

The dot product formulation is symmetric: dotProduct vec (G.adjMatrix α G v) equals the neighbor-sum expression.

Русский

Формула скалярного произведения симметрична: dotProduct vec (G.adjMatrix α G v) равно сумме по соседям.

LaTeX

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

Lean4

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

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