OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPauliProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact Pauli multiplication, including the scalar phases needed to replace a YY interaction by commuting real X/Z factors.

  1. def OAI.ContinuumCoulomb.qmaPauliProductIndex line 13
  2. def OAI.ContinuumCoulomb.qmaPauliProductPhase line 16
  3. theorem OAI.ContinuumCoulomb.qmaPauli_product line 20
  4. theorem OAI.ContinuumCoulomb.qmaPauliWord_product line 28