Zulip Chat Archive
Stream: mathlib4
Topic: Operators for `mulVec` and `vecMul`
Martin Dvořák (Jan 14 2024 at 15:19):
I don't like writing mulVec and vecMul in words. What about creating infix operators for them?
Eric Wieser (Jan 14 2024 at 15:37):
It probably makes sense to resume the previous discussion
Last updated: May 02 2025 at 03:31 UTC