Lean, informalized

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

Exercise 2.44 - The anticommutator, and an element that both commutes and anticommutes with an invertible one

Commuting and anticommuting with an invertible operator forces 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

Let AA and BB be operators on the same vector space, with AA invertible, and suppose that they commute, AB=BAAB = BA, and at the same time anticommute, AB=−BAAB = -BA. The exercise is to show that BB is then the zero operator.

Commutator and Anticommutator

The anticommutator {A,B}\{A,B\} of two elements AA and BB of a set with an addition and a multiplication, such as the operators on a vector space, is the sum of their two products taken in either order: {A,B}=AB+BA.\{A,B\} = AB + BA .(1)✦ A set with an addition and a multiplication, obeying the usual rules of arithmetic, is called a ring; the commutator [A,B][A,B] of two elements AA and BB of a ring is the difference of the same two products, AB−BAAB - BA.

The Claim

Theorem 1. Let RR be a ring in which 22 has an inverse, and let AA and BB be elements of RR with AA invertible. Then [A,B]=0and{A,B}=0⇒B=0.[A,B] = 0 \quad\text{and}\quad \{A,B\} = 0 \quad\Longrightarrow\quad B = 0 .(2)✦

The linear operators on a complex vector space form such a ring, and for them this is the exercise.

What Is Checked

The claim is stated over the anticommutator (1) and the commutator. What the library proves about these two brackets is (2).