Generated formalization-status view. Do not edit this section by hand.
The interim legacy catalogue remains authoritative until Issue #5228.
Canonical record detail
The Pauli X matrix squares to the identity.
- Record ID
- tasaki-2020-section-2-1-pauli-x-involutive
- Lean declaration
- LatticeSystem.Quantum.pauliX_mul_self
- Declaration kind
- theorem
- Human status
- proved
- Implementation state
- implemented
- Source coverage
- complete
- Trust state
- axiom_free
- Capstone
- false
- Module
- LatticeSystem.Quantum.Pauli
- Source path
- LatticeSystem/Quantum/Pauli.lean
- Origin
- literature
- Topic
- quantum-spin
- Axiom dependency
- none
- Proof-guide anchor
- none
- Citation
- Physics and Mathematics of Quantum Many-Body Systems, equation 2.1.8; section 2.1; equations 2.1.8; pages 15 — Pauli matrices for spin one-half
- Citation
- Quantum Computation and Quantum Information, exercise 2.41; section 2.1.3; pages 78 — Pauli involutivity and anticommutation