mul_adjMatrix_apply — Mathlib

English

The product of a matrix M with the adjacency matrix on the right yields a sum over neighbors with M's row fixed.

Русский

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

LaTeX

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

Lean4

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

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