Provedcommons

σx σy = i σz

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{pauliX}} \cdot \htmlData{mx=1}{\operatorname{pauliY}}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\htmlData{mx=3}{i} \, \htmlData{mx=4}{\operatorname{pauliZ}}}

What the notation means · or point at any symbol

pauliX: Commons.pauliX: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.pauliX)
·Multiplication: pauliX times pauliY. (Commons.pauliX * Commons.pauliY)
=Equality: pauliX · pauliY and I • pauliZ are the same. (Commons.pauliX * Commons.pauliY = Compl…)
pauliY: Commons.pauliY: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.pauliY)
iImaginary unit: The complex number i, with i² = −1. (Complex.I)
•Scalar multiplication: pauliZ scaled by the number I. (Complex.I • Commons.pauliZ)
pauliZ: Commons.pauliZ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.pauliZ)

theorem pauli-xy-is-i-z :
    Commons.pauliX * Commons.pauliY = Complex.I • Commons.pauliZ

From our commons: Commons.pauliX_mul_pauliY in the Commons.Physics.Pauli definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 9 lines of Lean