How to write repeated tensor products

Stream: mathlib4

[Jason Rute]

This PA.SX question is about how to naturally write things like $g : A_1 \otimes \cdots \otimes A_n \to B$. While I could give some answer using List and foldr/foldl, I assume there might be a more canonical solution in this case.

[Adam Topaz]

We have docs#PiTensorProduct

[Adam Topaz]

I see now that the question is about tensor products in a monoidal category, and there is indeed no canonical way yet. The default would be to associate to the right, similarly to how products work at the type level.