Zulip Chat Archive

Stream: PR reviews

Topic: !4#3287

Jeremy Tan (Apr 05 2023 at 11:55):

!4#3287 can somebody help fix the last error here?

theorem adjMatrix_vecMul_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
    ((G.adjMatrix α).vecMul vec) v = ∑ u in G.neighborFinset v, vec u := by
  rw [← dotProduct_adjMatrix, vecMul]
  refine' congr rfl _; ext
  rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

Last updated: Dec 20 2023 at 11:08 UTC