dot product commutative?

Stream: general

[victoria]

Is there a direct way to show the below?

variable {n m:ℕ} [NeZero m]
example (x: Fin n → ℝ )(y: Fin n → ℝ): x ⬝ᵥ y = y ⬝ᵥ x := by sorry

[Yury G. Kudryashov]

Unfold the definition and use commutativity of multiplication?

[victoria]

how to use unfold here?

[Eric Wieser]

The result is already in the library as docs#Matrix.dotProduct_comm

[Kevin Buzzard]

If you make a #mwe then it will be much easier for others to answer the question "how to use unfold here?".