Solèr’s theorem says that for every star division ring $R$ and every $R$-module $H$ with a orthomodular hermitan form $\langle (-),(-) \rangle:H \times H \to R$ such that there exists an infinite orthonormal sequence $e:\mathbb{N} \to H$, $R$ is either one of the the real numbers $\mathbb{R}$, the complex numbers $\mathbb{C}$, or the quaternions $\mathbb{H}$, and $H$ is a Hilbert space over $R$. Assuming that the star division rings used are Heyting division rings (or else Solèr’s theorem is most likely false), is Solèr’s theorem true in constructive mathematics?