Tensor products of Hilbert spaces?

Stream: Is there code for X?

[Kim Morrison]

We don't have the tensor product of Hilbert spaces (or even inner product spaces), right?

[Jireh Loreaux]

I think that's correct. Although we arguably have the tensor product with l2 in the file Mathlib.Analysis.InnerProductSpace.l2Space

[Heather Macbeth]

See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Tensor.20products.20of.20inner.20product.20spaces for previous discussion ...