Stream: Is there code for X?
Hanting Zhang (Jan 01 2021 at 17:53):
I haven't found this in mathlib explicitly.
Eric Wieser (Jan 01 2021 at 18:45):
I think it's not there. We have antisymmetric maps as docs#alternating_map
Eric Wieser (Jan 01 2021 at 19:02):
*linear maps, that is
Last updated: May 16 2021 at 05:21 UTC