OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListLatticeProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Literal source serialization from the computed coordinate and bond tapes.

  1. abbrev OAI.ContinuumCoulomb.QuantumListLattice.Input line 12
  2. def OAI.ContinuumCoulomb.QuantumListLattice.inputCode line 13
  3. def OAI.ContinuumCoulomb.QuantumListLattice.packet line 16
  4. def OAI.ContinuumCoulomb.QuantumListLattice.value line 18
  5. def OAI.ContinuumCoulomb.QuantumListLattice.coordinateProgram line 20
  6. def OAI.ContinuumCoulomb.QuantumListLattice.packetProgram line 25
  7. def OAI.ContinuumCoulomb.QuantumListLattice.program line 37
  8. theorem OAI.ContinuumCoulomb.QuantumListLattice.value_source line 40
  9. theorem OAI.ContinuumCoulomb.QuantumListLattice.value_valid line 57
  10. theorem OAI.ContinuumCoulomb.QuantumListLattice.value_mem_yes line 64
  11. theorem OAI.ContinuumCoulomb.QuantumListLattice.value_mem_no line 77