Thoughts on the definition of Hilbert Space and Bra-Ket

Version bump

1. Why PhysLean decides to define finite Hilbert Space and infinite Hilbert Space separately?
2. We try to define Ket as a linear map (eg. noncomputable def Ket: ℂ →ₗ[ℂ] H := (innerSL ℂ 1).toLinearMap.smulRight ψ), so that we can use the uniform notation tensor product of map (eg. f "⊗ₘ" g => TensorProduct.map f g) for calculation like this: ((⟨ψ| ⊗ₘ ⟨φ|) ∘ₛₗ (|ψ⟩ ⊗ₘ |φ⟩)). And also, Ket definition can both used for infinite Hilbert Space and finite Hilbert Space. How do you think of this definition? What are pros and cons of doing this?

Start by reviewing the existing finite and infinite Hilbert Space definitions and the proposed Ket linear-map definition described in the issue. Compare the notation and tensor-product composition goals, then establish and document the project direction for supporting both cases.