V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun i => adjMatrix α G i v) = (fun u => vec u) ⬝ᵥ adjMatrix α G v
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vecMul vec (adjMatrix α G) v = ∑ u in neighborFinset G v, vec u
simp only [← dotProduct_adjMatrix, vecMul]
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i => adjMatrix α G i v) = adjMatrix α G v
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun i => adjMatrix α G i v) = (fun u => vec u) ⬝ᵥ adjMatrix α G v
refine' congr rfl _
case h
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i => adjMatrix α G i v) = adjMatrix α G v
ext x
no goals
case h
V : Type u_2
α : Type u_1
β : Type ?u.43997
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x
rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]