Tensor product of bounded operators

Stream: mathlib4

[Magalame]

Sorry, this might be a bit trivial but is there already a theorem in mathlib about how (X →L[ℂ] X) ⊗ (Y →L[ℂ] Y) = X ⊗ Y →L[ℂ] X ⊗ Y, with X,Y hilbert spaces?

[Henrik Böving]

There is close to 0 mathematics in mathlib 4 right now you will most likely have better luck if you ask the mathlib 3 people in #general though

[Magalame]

oh I see thanks!