Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 76
Exercise2.36 - The matrices of
and
and the vanishing of their traces
The Pauli matrices
and
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 ,, in which an operator on the qubit is written as a complex matrix. The exercise asks to show that two of the Pauli matrices, written and below, have trace zero: for each, the sum of its two diagonal entries vanishes.
The Pauli Matrices
The Pauli matrix is the complex matrix (1)✦
The Pauli matrix is the complex matrix (2)✦ with the imaginary unit.
The Claim
Theorem 1. The Pauli matrices of (1) and of (2) satisfy (3)✦ and (4)✦
What Is Checked
The claim is stated over the two matrices (1) and (2), with complex entries, and takes no hypothesis.