Assuming [Bishop's](http://www.springer.com/gp/book/9783642649059) constructive mathematics, is it true that any real-valued square matrix with **distinct** roots of the characteristic polynomial can be diagonalized? By distinct, I mean **apart**: $x \neq y \triangleq \exists q \in \mathbb{Q}.|x - y| > q$. (There may be similar defnitions)


For the case $n=2$, it seems true since we can deduce $a\_{11} - \lambda\_j \neq 0 \lor a\_{22} - \lambda\_j \neq 0$ for any $j = 1, 2$ where $a\_{ii}, i=1,2$ are the diagonal elements and $\lambda\_j$s are the roots of the characteristic polynomial. It then allows multiplying by a nonzero number and, using the property that $(a\_{11} - \lambda\_j)(a\_{22} - \lambda\_j) = a\_{12}a\_{21}$, solving the respective system of linear equations and consequently finding an eigenvector: $A v = \lambda\_j v$. 


Already for the case $n=3$, the argument seems not to work and one cannot proceed without some case distinction on reals. [This work](http://ac.els-cdn.com/0168007286900060/1-s2.0-0168007286900060-main.pdf?_tid=f7d5faaa-c5ca-11e6-9674-00000aab0f27&acdnat=1482138801_34d65d1543ed9d625fe261e2606b9cd1) addresses the problem in Lemma 1.5, but they seem to assume $xy = 0 \implies x =0 \lor y=0$ which is not valid constructively.


[Coquand and Lombardi](http://www.cse.chalmers.se/~coquand/FISCHBACHAU/AlgebraLogicCoqLom.pdf) in Theorem 2.3 constructed an effective procedure of finding eigenvectors of a projection matrix. I suspected that something like this could be done for general matrices where it is known beforehand that the roots of the characteristic polynomial are distinct. 


[Lombardi and Quitte](https://arxiv.org/pdf/1605.04832.pdf) addressed the problem on page 100 (top). Also in Proposition 5.3, they claim that 


$$\prod\_{i=1}^n ( (A - \lambda\_i I)\_{1 \dots n-1, 1 \dots n-1} ) \neq 0$$


by "exhibiting" the companion matrix of $\lambda^n - 1$. Their language is a bit obscure. However, it seems they imply the following lemma:


*Let $A = M(\mathbb{R},n)$, and suppose that the roots $\lambda\_1, \dots, \lambda\_n$ of the charteristic polynomial for $A$ are mutually apart. Then, for every root $\lambda\_j$ of the characteristic polynomial, there is a principal submatrix of $A - \lambda\_j I$ of size $(n-1) \times (n-1)$ which is invertible.*



Matrix diagonalization and eigenvector computation constructively
The following works constructively over an arbitrary local ring $R$ (constructively, $\mathbb{R}$ is a local ring).


Assume that you matrix $M$ is canceled by a polynomial $Q$, of degree $m$ (with leading coefficent $1$), that $Q$ can be factored into


$$Q= \prod^m\_{i=1}(X-q\_i)$$


and that for each $i \neq j$, $(q\_i - q\_j)$ is invertible (in the case of $\mathbb{R}$ it just means that $q\_i$ and $q\_j$ are appart).


Then one can diagonalize $M$. In particular it can be applied when you have some multiplicites in your eigenvalue as long as the minimal polynomial has simple roots.


Let 
$$P\_i = \frac{\displaystyle \prod\_{j \neq i} (X-q\_j)}{ \displaystyle \prod\_{j \neq i} (q\_i-q\_j)} $$


i.e. $P\_i(q\_i)=1$ and if $i \neq j$ , $P\_i(q\_j)=0$


It is constructive that a polynomial is divisibe by $Q$ if and only if it vanishes at all the $q\_i$ (basically because polynomial division by a polynomial with unit leading coefficient works well). Hence you can easily check that:


$(P\_i)^2 - P\_i$


$P\_i P\_j$


$1-\sum\_i P\_i$


$X-\sum\_i q\_i P\_i$


are all divisible by $Q$ and hence cancel $M$.
So the $P\_i(M)$ form a complete family of projection, and $M = \sum q\_i P\_i(M)$ and you get the spectral decomposition of $M$.


At this point, if you already know how to find eigen vectors for projections then you are done: the range of each $P\_i$ are in direct sum so you just find a basis of each of these subspaces and you get your diagonal basis.


I have not read the paper by Coquand & Lombardi you are quoting so I'm not sure what is their method for the last step. I know of a process for this that work for local ring of 'zero residual characteristic' (i.e. in which integer are invertible sot ) I'm not sure what happen in the fully general case, but it is already enough for the case of $\mathbb{R}$.


