Lean, informalized

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

Exercise 2.1 - Three vectors with given components satisfy a linear relation with coefficients not all zero

Three dependent vectors in two complex dimensions.

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

The vectors |v1⟩|v_1\rangle, |v2⟩|v_2\rangle and |v3⟩|v_3\rangle of Exercise 2.1 are the three vectors of the Hilbert space ℂ2\mathbb{C}^2 of pairs of complex numbers with components |v1⟩=(1,−1),|v2⟩=(1,2),|v3⟩=(2,1).|v_1\rangle = (1,-1), \qquad |v_2\rangle = (1,2), \qquad |v_3\rangle = (2,1).(1)✦ The exercise asks to show that they are linearly dependent.

The Claim

Theorem 1. The vectors |v1⟩|v_1\rangle, |v2⟩|v_2\rangle and |v3⟩|v_3\rangle of (1) are linearly dependent: there are complex numbers a1a_1, a2a_2 and a3a_3, not all zero, with a1|v1⟩+a2|v2⟩+a3|v3⟩=0.a_1|v_1\rangle + a_2|v_2\rangle + a_3|v_3\rangle = 0.(2)✦

What Is Checked

The claim is stated over the triple |v1⟩|v_1\rangle, |v2⟩|v_2\rangle, |v3⟩|v_3\rangle of (1) and over linear dependence with complex coefficients. What the library proves about this triple is the dependence (2), with no hypotheses.