The Exercise

An operator $A$ on the state space of a quantum system becomes a matrix once an orthonormal basis is chosen, and another basis gives another matrix. Take two orthonormal bases $\{|v_i\rangle\}$ and $\{|w_i\rangle\}$ of the space, and let $A'$ and $A''$ be the matrices of $A$ in the first and in the second. The exercise asks how $A'$ and $A''$ are related.

Matrices in an Orthonormal Basis

The library works on a finite-dimensional inner product space $V$ over the real or the complex numbers, with two orthonormal bases $\{|v_i\rangle\}$ and $\{|w_i\rangle\}$ indexed by the same finite set.

The matrix $A'$ of a linear operator $A$ on $V$ in the orthonormal basis $\{|v_i\rangle\}$ is the square matrix of the matrix elements of $A$ between basis vectors, $$A'_{ij} = \langle v_i | A | v_j \rangle ,$$(1) The matrix $A''$ of $A$ in the orthonormal basis $\{|w_i\rangle\}$ is the square matrix of the matrix elements of $A$ between basis vectors, $A''_{ij} = \langle w_i | A | w_j \rangle$.

The change of basis matrix $U$ from $\{|v_j\rangle\}$ to $\{|w_i\rangle\}$ is the square matrix whose $j$th column holds the coordinates of $|v_j\rangle$ in the basis $\{|w_i\rangle\}$, $$U_{ij} = \langle w_i | v_j \rangle .$$(2)

The Claim

What Is Checked

The claim is stated over a linear operator on a finite-dimensional real or complex inner product space, two orthonormal bases of that space, the matrices (1) of the operator in each, and the change of basis matrix (2) between the bases.

What the library proves about them is the relation (3), for every linear operator and every pair of orthonormal bases.