adjMatrix_mulVec_const_apply — Mathlib

English

Multiplying the adjacency matrix by a constant vector yields the degree times the constant.

Русский

Умножение матрицы смежности на константный вектор даёт степень вершины, умноженную на константу.

LaTeX

$$(G.adjMatrix α *ᵥ Function.const _ a) v = G.degree v * a$$

Lean4

theorem adjMatrix_mulVec_const_apply [NonAssocSemiring α] {a : α} {v : V} :
    (G.adjMatrix α *ᵥ Function.const _ a) v = G.degree v * a := by simp

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