Can Hilbert spaces be defined over fields other than $\mathbb R$ and $\mathbb C$? Let $V$ be a vector space over a field $K$. Suppose further that $K$ has the following structures:

*

*$K$ has a subfield $K_{\mathbb R}$ equipped with a field embedding $K_{\mathbb R}\hookrightarrow\mathbb R$, so we can identity elements of $K_{\mathbb R}$ with elements of $\mathbb R$.


*$K$ has an involution $*:K\to K,z\mapsto z^*$, meaning $*$ is an automorphism and that $(z^*)^*=z$ for all $z\in K$.
Define a $(K,K_{\mathbb R},*,\hookrightarrow)$-inner product space $\big(V,(K,K_{\mathbb R},*,\hookrightarrow),\langle\cdot,\cdot\rangle\big)$ as a $K$-vector space (where $*,K_{\mathbb R},$ and $\hookrightarrow$ are the structures described above) together with a map $\langle\cdot,\cdot\rangle:V\times V\to K$ that satisfies the following properties:

*

*$\langle x,y\rangle=\langle y,x\rangle^*$ for all $x,y\in V$.

*$\langle x,\cdot\rangle:V\to K$ is linear for all fixed $x\in V$.

*$\forall x\in V\setminus\{0\}:\langle x,x\rangle>0$.

Condition (3) should be interpreted as saying $\langle x,x\rangle\in K_{\mathbb R}$ and the embedding (discussed above) identifies $\langle x,x\rangle$ with a positive real number.
The idea of this definition is to allow for inner products to be defined in the most general setting possible and still agree with the usual definitions for $\mathbb R$ and $\mathbb C$.
Define a $(K,K_{\mathbb R},*,\hookrightarrow)$-Hilbert space as a $(K,K_{\mathbb R},*,\hookrightarrow)$-inner product space in which the induced norm $\lVert x\rVert =\sqrt{\langle x,x\rangle}$ makes $V$ into a complete metric space.
Do there exist nontrivial$^\dagger$ $(K,K_{\mathbb R},*,\hookrightarrow)$-Hilbert spaces for any fields $K\neq\mathbb R$ or $\mathbb C$?
The "$\neq$" should be read as "not isomorphic to." If yes, that would suggest interesting possible extensions of the usual definition of Hilbert space; if no, that would provide a justification for only ever defining or considering Hilbert spaces over $\mathbb R$ and $\mathbb C$.

$^\dagger$ By non-trivial, I mean $V\neq\{0\}$, the single-element vector space.
 A: Let us assume for convenience that the embedding $K_\mathbb{R}\to\mathbb{R}$ is actually the inclusion map of a subfield of $\mathbb{R}$.  Suppose $V$ is any nontrivial $K$-Hilbert space and let $x\in V$ be nonzero.  For any $a\in K_\mathbb{R}$, we then have $\|ax\|^2=aa^*\|x\|^2$.  It follows that $a^*\in K_\mathbb{R}$ and $a^*$ has the same sign as $a$.  Thus $a\mapsto a^*$ is an order-preserving embedding of $K_\mathbb{R}$ into itself and therefore must be the identity (since it is the identity on $\mathbb{Q}$, which is order-dense in $K_\mathbb{R}$).  That is, $a^*=a$ for all $a\in K_\mathbb{R}$.  Now if $(a_n)$ is a sequence in $K_\mathbb{R}$ which converges to some $r\in\mathbb{R}$, the sequence $(a_nx)$ is Cauchy (since $\|a_nx-a_mx\|^2=(a_n-a_m)^2\|x\|^2$) and so converges to some $y\in V$.  By continuity of the distance function on $V$, we must have $\|y\|^2=\lim_n \|a_nx\|^2=r^2\|x\|^2$.  Since $r\in\mathbb{R}$ here is arbitrary, we have shown that the function $y\mapsto \langle y,y\rangle$ takes every nonnegative real value.  Thus in fact $K_\mathbb{R}$ must be all of $\mathbb{R}$.
Now our field $K$ is an extension of $\mathbb{R}$ with an involutive automorphism $a\mapsto a^*$ which fixes $\mathbb{R}$ pointwise.  Conversely, for any $a\in K$ such that $a=a^*$, we have $\|ax\|^2=a^2\|x\|^2\geq 0$ and thus $a^2\geq 0$, which implies $a\in\mathbb{R}$.  That is, $\mathbb{R}$ is exactly the fixed field of the automorphism $a\mapsto a^*$.  Thus $K$ is an extension of $\mathbb{R}$ of degree at most $2$ (specifically, of degree equal to the size of the group of automorphisms generated by $a\mapsto a^*$), and so it can only be $\mathbb{R}$ or $\mathbb{C}$.
