adjMatrix_mul_apply — Mathlib

English

The product of an arbitrary matrix M with the adjacency matrix on the left yields a sum over neighbors.

Русский

Произведение произвольной матрицы M на слева матрицы смежности даёт сумму по соседям.

LaTeX

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

Lean4

@[simp]
theorem adjMatrix_mul_apply [NonAssocSemiring α] (M : Matrix V V α) (v w : V) :
    (G.adjMatrix α * M) v w = ∑ u ∈ G.neighborFinset v, M u w := by
  simp [mul_apply, neighborFinset_eq_filter, sum_filter]

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