mathlib

mathlib copied to clipboard

Follow-up from #4771:

we should redefine tensor_product.map to be [a] bundled hom. And linear_map.tensor can enable the notation f.tensor g.

Can we do anything to make that notation f ⊗ₜ g instead? (And is that a good idea?)

If we work in the category Module R, then that notation already works. It would be good to make it as easy as possible to shift back and forth between the two points of view.