adjMatrix_mulVec_const_apply_of_regular

English

If G is regular of degree d, then (G.adjMatrix α *ᵥ a) v = d · a.

Русский

Если граф G регулярного степени d, то (G.adjMatrix α *ᵥ a) v = d · a.

LaTeX

$$G.IsRegularOfDegree d → (G.adjMatrix α *ᵥ Function.const V a) v = d.cast a$$

Lean4

theorem adjMatrix_mulVec_const_apply_of_regular [NonAssocSemiring α] {d : ℕ} {a : α} (hd : G.IsRegularOfDegree d)
    {v : V} : (G.adjMatrix α *ᵥ Function.const _ a) v = d * a := by simp [hd v]

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