OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRowTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Moving a complete register between two disjoint rows.

  1. def OAI.ContinuumCoulomb.qmaRowPairs line 11
  2. theorem OAI.ContinuumCoulomb.qmaRowPairs_disjoint line 14
  3. theorem OAI.ContinuumCoulomb.qmaRowPairs_distinct line 22
  4. theorem OAI.ContinuumCoulomb.qmaRowTransfer_coordinates line 28
  5. theorem OAI.ContinuumCoulomb.qmaRowTransfer_fixed line 36
  6. theorem OAI.ContinuumCoulomb.qmaRowTransfer_involutive line 44
  7. theorem OAI.ContinuumCoulomb.qmaRowTransfer_matrix line 61
  8. theorem OAI.ContinuumCoulomb.qmaRowTransfer_length line 67