Diagonalizable exactly when there is an eigenbasis

For every field $K$ (an arbitrary type carrying a field structure, with no assumption of algebraic closure, characteristic, or ordering), every natural number $n$ (including $n = 0$), and every square matrix $A \in K^{n \times n}$ whose rows and columns are indexed by the $n$-element index type $\{0, 1, \dots, n-1\}$, the following two existence statements are equivalent (a genuine two-directional "if and only if", not an implication in one direction):

• Left side. There exist a matrix $P \in K^{n \times n}$ and a function $d : \{0,\dots,n-1\} \to K$ such that $\det P$ is a unit of $K$ — equivalently, since $K$ is a field, $\det P \neq 0$ — and $P^{-1} A P = \operatorname{diag}(d_0, \dots, d_{n-1})$, the matrix whose $(i,i)$ entry is $d_i$ and whose off-diagonal entries are $0$. Here $P^{-1}$ denotes the total inversion operation on matrices (which would return the zero matrix for a singular argument), but the accompanying invertibility hypothesis forces it to be the genuine two-sided inverse of $P$; note also the specific order of the product, $P^{-1}$ on the left and $P$ on the right.

• Right side. There exist a basis $B$ of the $K$-vector space $K^{n}$ of functions $\{0,\dots,n-1\} \to K$, indexed by $\{0,\dots,n-1\}$ (so it consists of exactly $n$ vectors $B_0, \dots, B_{n-1}$), and a function $\lambda : \{0,\dots,n-1\} \to K$, such that for every index $i$ the matrix–vector product satisfies

where $A B_i$ is the usual left action of the matrix on a column vector and $\lambda_i \cdot B_i$ is scalar multiplication.

Several things the quantifiers silently permit should be made explicit: the scalars $d_i$ and $\lambda_i$ are unconstrained elements of $K$ and may be zero, repeated, or all equal; no relationship (equality, permutation, or matching multiplicities) is asserted between the diagonal entries $d$ produced on one side and the scalars $\lambda$ produced on the other, nor between $P$ and $B$; the basis vectors $B_i$ are automatically nonzero and linearly independent by virtue of forming a basis, but no normalization, orthogonality, or ordering condition is imposed; and in the degenerate case $n = 0$ both sides hold trivially (the unique $0 \times 0$ matrix has determinant $1$, and the empty family is a basis of the zero space, with the universally quantified condition holding vacuously), so the equivalence carries no content there. The statement is asserted for the fixed matrix $A$ supplied as an argument, with $K$, $n$, and the field structure on $K$ inferred rather than stated by the user; it claims only the equivalence of the two existence statements and does not exhibit or construct either $P$, $d$, $B$, or $\lambda$.