Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 76

Exercise 2.36 - The matrices of XX and YY and the vanishing of their traces

The Pauli matrices XX and YY have trace zero.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A single qubit has the computational basis |0⟩|0\rangle, |1⟩|1\rangle, in which an operator on the qubit is written as a complex 2×22 \times 2 matrix. The exercise asks to show that two of the Pauli matrices, written XX and YY below, have trace zero: for each, the sum of its two diagonal entries vanishes.

The Pauli Matrices

The Pauli XX matrix is the complex 2×22 \times 2 matrix X=(0110).X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}.(1)✦

The Pauli YY matrix is the complex 2×22 \times 2 matrix Y=(0−ii0),Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix},(2)✦ with ii the imaginary unit.

The Claim

Theorem 1. The Pauli matrices XX of (1) and YY of (2) satisfy trX=0\mathrm{tr}\,X = 0(3)✦ and trY=0.\mathrm{tr}\,Y = 0.(4)✦

What Is Checked

The claim is stated over the two matrices (1) and (2), with complex entries, and takes no hypothesis.