OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumWireIntertwining.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Intertwining identities for moving operators together with their active wires.

  1. theorem OAI.ContinuumCoulomb.qmaWirePermutation_mul_matrix line 12
  2. theorem OAI.ContinuumCoulomb.qmaMatrix_mul_wirePermutation line 24
  3. theorem OAI.ContinuumCoulomb.qmaWirePermutation_intertwines line 35
  4. theorem OAI.ContinuumCoulomb.qmaWireBasis_symm line 43
  5. theorem OAI.ContinuumCoulomb.qmaGate_wire_intertwines line 48
  6. theorem OAI.ContinuumCoulomb.qmaGateProduct_wire_intertwines line 55