Provedcommons

σx and σy anticommute

\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{pauliX}} \cdot \htmlData{mx=1}{\operatorname{pauliY}}} + \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{pauliY}} \cdot \htmlData{mx=4}{\operatorname{pauliX}}}} \mathrel{\htmlData{mx=7}{=}} 0

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)
+Addition: pauliX · pauliY plus pauliY · pauliX. (Commons.pauliX * Commons.pauliY + Commo…)
=Equality: pauliX · pauliY + pauliY · pauliX and 0 are the same. (Commons.pauliX * Commons.pauliY + Commo…)
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)

theorem pauli-x-y-anticommute :
    Commons.pauliX * Commons.pauliY + Commons.pauliY * Commons.pauliX = 0

From our commons: Commons.pauliX_anticomm_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