OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPauliTripleSplit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every real three-local Pauli word splits into one real factor and two single-site factors of the same entry parity.

  1. theorem OAI.ContinuumCoulomb.qmaPauliRestrict_restrict line 15
  2. theorem OAI.ContinuumCoulomb.qmaPauliYCount_zero line 23
  3. theorem OAI.ContinuumCoulomb.qmaThreeSupport_split line 26
  4. theorem OAI.ContinuumCoulomb.qmaPauliWord_triple_factor line 56