Unfold dot product

Stream: new members

[Martin Dvořák]

How can I prove this technical lemma, please?

variables {R : Type*} [comm_ring R]

lemma this_shoud_be_trivial (a b c d e f : R) :
matrix.dot_product ![a, b, c] ![d, e, f] = a*d + b*e + c*f
:= sorry

This question is related to (I am implementing the cross product):
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cross.20product

[Martin Dvořák]

This is the definition (from data.matrix.basic) I am referring to:

/-- `dot_product v w` is the sum of the entrywise products `v i * w i` -/
def dot_product [has_mul α] [add_comm_monoid α] (v w : m → α) : α :=
∑ i, v i * w i

[Damiano Testa]

by simp [add_assoc] seems to work.