Zulip Chat Archive

Stream: new members

Topic: vector multiplication

tsuki hao (Aug 09 2023 at 06:00):

I wonder how vector multiplication over R^n could be described in lean, will you be so kind to enlight me?

Johan Commelin (Aug 09 2023 at 07:04):

What does vector multiplication mean? Do you mean coordinatewise multiplication?

tsuki hao (Aug 09 2023 at 07:13):

Johan Commelin said:

What does vector multiplication mean? Do you mean coordinatewise multiplication?

a.png

Eric Wieser (Aug 09 2023 at 07:30):

Note that page is telling you that "vector multiplication" is ambiguous and you should use the words "dot product" instead

Johan Commelin (Aug 09 2023 at 08:28):

Additionally, note that "dotProduct" occurs very often in mathlib.

Last updated: Dec 20 2023 at 11:08 UTC