Provedcommons
σx squares to the identity
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 pauliX. (
Commons.pauliX * Commons.pauliX) - =Equality
- pauliX · pauliX and 1 are the same. (
Commons.pauliX * Commons.pauliX = 1)
theorem pauli-x-squares-to-one :
Commons.pauliX * Commons.pauliX = 1From our commons: Commons.pauliX_mul_self 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
Sign in to see the proofThe proof, its signed report and its history.