Let $H_1$ be a $\mathbb{C}$-Hilbert space and $H_2$ be a $\mathbb{R}$-Hilbert space, both assumed separable.
For any $\phi\in H_1,\psi\in H_2$ we may define the (bilinear? by the wikipedia definition this can't be bilinear since $H_1$ and $H_2$ has different scalar fields) mapping $\phi\otimes \psi:H_1\times H_2 \to \mathbb{C}$ by $$ \phi\otimes \psi(x,y) = \langle x,\phi \rangle_1 \langle y,\psi \rangle_2 $$ We note that since only $H_1$ has a complex inner product, we can in general for $\lambda\in \mathbb{C}$ only say that $$ \lambda (\phi \otimes \psi) = (\lambda \psi)\otimes \psi \quad \quad \text{and not}\quad \quad \lambda (\phi \otimes \psi) = \psi\otimes (\lambda\psi). $$ Anyways I have proven (I can add the proof, but i think it is correct) that we can create an inner product of the space $\mathcal{E}$ of all finite linear combinations of the bilinear mappings considered above, by letting $$ \langle \phi_1 \otimes \psi_1 , \phi_2\otimes \psi_2 \rangle = \langle\phi_1,\phi_2 \rangle_1 \langle\psi_1,\psi_2 \rangle_2 $$ and extending it to finite linear combinations in the following way $$ \Big\langle \sum_{i=1}^n a_i ( \phi_i\otimes \psi_i), \sum_{i=1}^m b_i (\beta_i \otimes \gamma_i) \Big\rangle = \sum_{i=1}^n \sum_{j=1}^m a_i \bar{b}_j \langle \phi_i\otimes \psi_i, \beta_j \otimes \gamma_j \rangle $$ We now define $H_1\otimes H_2$ as the completion of the space of finite linear combinations with respect to the metric induced by the above inner product. Furhtermore it is well-known that the above inner product can be extended to $H_1\otimes H_2$, such that it satisfies $$ \langle \iota(\phi\otimes \psi), \iota(\gamma\otimes \beta) \rangle_{H_1\otimes H_2} = \langle\phi_1,\gamma\rangle_1 \langle \psi,\beta\rangle_2 $$ for any $\phi,\gamma\in H_1$ and $\psi,\beta\in H_2$, where $\iota$ is the linear isometric embedding into the completion.
Question: Is this a valid construction of the tensor product of two Hilbert spaces with different fields? I could not find any mistake, but the ideas are taken from some notes that considers two real Hilbert spaces. Also every source of the tensor product of Hilbert spaces that I have encountered considers either two real or two complex Hilbert spaces, which is why I'm worried I have made a mistake.
Edited to reflect only the above question remains.