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: Dec 20 2025 at 21:32 UTC