degMatrix_mulVec_apply — Mathlib

English

Multiplying the degree matrix by a vector vec gives a vector whose i-th component is deg(i)·vec(i).

Русский

Умножение диагональной матрицы степеней на вектор vec даёт в i-й компоненте deg(i)·vec(i).

LaTeX

$$$(G.degMatrix R *\!\vec{R})_v = G.degree(v) * \vec{v}$$$

Lean4

theorem degMatrix_mulVec_apply [NonAssocSemiring R] (v : V) (vec : V → R) :
    (G.degMatrix R *ᵥ vec) v = G.degree v * vec v := by rw [degMatrix, mulVec_diagonal]

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