OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedBasis.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Splitting the original register from fresh grid wires.

  1. def OAI.ContinuumCoulomb.qmaAppendBasis line 12
  2. def OAI.ContinuumCoulomb.qmaPaddedIndex line 22
  3. def OAI.ContinuumCoulomb.qmaPaddedBasis line 25
  4. def OAI.ContinuumCoulomb.qmaPaddedLeft line 30
  5. def OAI.ContinuumCoulomb.qmaPaddedRight line 33
  6. theorem OAI.ContinuumCoulomb.qmaPaddedLeft_injective line 36
  7. theorem OAI.ContinuumCoulomb.qmaPaddedLeft_ne_right line 39
  8. theorem OAI.ContinuumCoulomb.qmaPaddedBasis_left line 47
  9. theorem OAI.ContinuumCoulomb.qmaPaddedBasis_right line 50
  10. theorem OAI.ContinuumCoulomb.qmaPaddedBasis_symm_left line 53
  11. theorem OAI.ContinuumCoulomb.qmaPaddedBasis_symm_right line 58
  12. theorem OAI.ContinuumCoulomb.sourceTensor_padded line 63