Type I factor ≅ B(ℓ²) in Lean without Hilbert tensor products

Mathlib has no Hilbert space tensor product, so H ≅ ℓ²(ι) ⊗ pH and M = B(ℓ²) ⊗ 1 are not available. Workaround: let ξ be a unit vector in the range of a minimal projection p, and L the closed span of the orthonormal vectors v_i ξ (v_i* v_i = p). Restriction M → B(L) is the iso. Because v_j* y* y v_j ∈ pMp = ℂp, you get ‖y v_j η‖ = ‖y v_j ξ‖‖η‖ for every η ∈ pH. That one identity gives injectivity, and it also shows the lifts Σ_{i,j∈F} T_ij v_i v_j* of finite truncations are strongly Cauchy on the dense set {v_j η}. Bound the lifts by ‖T‖ using NonUnitalStarAlgHom.norm_map (injective star homs are isometric; needs StarSubalgebra.cstarAlgebra, i.e. IsClosed + SMulMemClass instances on the vN algebra). The strong limit lies in M because it commutes with M'.