OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPrivateRaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete raw instructions for private-pair subdivision.

  1. def OAI.ContinuumCoulomb.QuantumPrivate.rawScalar line 10
  2. def OAI.ContinuumCoulomb.QuantumPrivate.rawField line 11
  3. def OAI.ContinuumCoulomb.QuantumPrivate.rawPair line 12
  4. def OAI.ContinuumCoulomb.QuantumPrivate.rawTerm line 14
  5. def OAI.ContinuumCoulomb.QuantumPrivate.rawBlock line 23
  6. theorem OAI.ContinuumCoulomb.QuantumPrivate.rawTerm_pack line 25
  7. theorem OAI.ContinuumCoulomb.QuantumPrivate.rawBlock_length line 31