The Exercise

Take a qubit and a circuit of three gates on it: a Hadamard gate $H$, then one of the Pauli gates $X$, $Y$ or $Z$, then a second Hadamard gate. The circuit acts on the qubit as the product $HXH$, $HYH$ or $HZH$, and the exercise asks which single gate each of these three products is.

The Gates as Matrices

Each gate is written as its matrix in the computational basis $|0\rangle, |1\rangle$ of the qubit. The Pauli matrices $X$, $Y$ and $Z$ are the complex $2 \times 2$ matrices $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix},$$(1) with $i$ the imaginary unit. The Hadamard matrix $H$ is the complex $2 \times 2$ matrix $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}.$$(2)^✦

The Claim

What Is Checked

The theorem is stated over the matrices (1) and (2) and assumes nothing else about them. About these matrices the library proves the identities (3), (4) and (5), each an equality of $2 \times 2$ matrices under the matrix product.