OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawExchange.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Raw, rational finite-list instructions for the four-spin compiler.

  1. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.Raw line 11
  2. def OAI.ContinuumCoulomb.QuantumRawExchange.rawCode line 12
  3. def OAI.ContinuumCoulomb.QuantumRawExchange.axis line 16
  4. def OAI.ContinuumCoulomb.QuantumRawExchange.pack line 18
  5. theorem OAI.ContinuumCoulomb.QuantumRawExchange.axis_pack line 24
  6. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.Environment line 27
  7. def OAI.ContinuumCoulomb.QuantumRawExchange.environmentCode line 28
  8. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.Input line 29
  9. def OAI.ContinuumCoulomb.QuantumRawExchange.inputCode line 30
  10. def OAI.ContinuumCoulomb.QuantumRawExchange.field line 32
  11. def OAI.ContinuumCoulomb.QuantumRawExchange.cross line 35
  12. def OAI.ContinuumCoulomb.QuantumRawExchange.bonds line 40
  13. def OAI.ContinuumCoulomb.QuantumRawExchange.scalar line 53
  14. theorem OAI.ContinuumCoulomb.QuantumRawExchange.bonds_length line 58
  15. theorem OAI.ContinuumCoulomb.QuantumRawExchange.bonds_pack_length line 64