quantum_commutator_self_adjoint_skew
theoremverified
The commutator [A, B] = A * B - B * A of two self-adjoint continuous linear operators A and B on a complex Hilbert space is skew-adjoint, that is, star ⁅A, B⁆ = -⁅A, B⁆.
Statement
theorem quantum_commutator_self_adjoint_skew {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A B : E →L[ℂ] E) (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B) : star ⁅A, B⁆ = -⁅A, B⁆
- Source
- Hall, Quantum Theory for Mathematicians, Section 3.4
- Verified
- 11 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Read back from the Lean
Let $E$ be a complete complex normed inner product space (a complex Hilbert space). For any continuous linear operators $A, B : E \to E$, if $A$ is self-adjoint and $B$ is self-adjoint, then the adjoint (star) of their commutator (Lie bracket) $\llbracket A, B \rrbracket$ is equal to $-\llbracket A, B \rrbracket$ (that is, the commutator is skew-adjoint).
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The commutator of two self-adjoint operators is skew-adjoint (anti-self-adjoint). -/ theorem quantum_commutator_self_adjoint_skew {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A B : E →L[ℂ] E) (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B) : star ⁅A, B⁆ = -⁅A, B⁆ := by simp only [Ring.lie_def, star_sub, star_mul, hA.star_eq, hB.star_eq] abel