Assuming Bishop's 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 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 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 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.*