no goals
V : Type u_2
α : Type u_1
β : Type ?u.66478
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : Semiring α
d : ℕ
a : α
hd : IsRegularOfDegree G d
v : V
⊢ mulVec (adjMatrix α G) (Function.const V a) v = ↑d * a
simp [hd v]