About PiTensor Product and Tensor Product

Stream: new members

[Pumpkin678]

$$Can\ V\bigotimes V \ be\ expressed \ in\ lean4\ as\ T^2V\ ?$$

[Notification Bot]

Pumpkin678 has marked this topic as resolved.

[Notification Bot]

Pumpkin678 has marked this topic as unresolved.

[Eric Wieser]

@loogle TensorProduct, PiTensorProduct

[loogle]

:search: PiTensorProduct.tmulEquiv, PiTensorProduct.tmulEquiv_apply, and 1 more

[Eric Wieser]

Looks like the answer is no, we only have $T^nV \otimes T^mV \cong T^{m+n}V$ and $T^1V \cong V$

[Eric Wieser]

So you can glue those together, but it is likely just as easy to write the isomorphism directly using the respective universal properties.