OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryEnumeration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit consecutive labels for every term in the distributed history.

  1. def OAI.ContinuumCoulomb.qmaUnitFin line 13
  2. abbrev OAI.ContinuumCoulomb.qmaHistoryReferenceWork line 19
  3. def OAI.ContinuumCoulomb.qmaHistoryTermIndex line 21
  4. def OAI.ContinuumCoulomb.qmaHistoryReferenceTerms line 29
  5. theorem OAI.ContinuumCoulomb.qmaHistoryReferenceTerms_sum line 34
  6. theorem OAI.ContinuumCoulomb.qmaHistoryReferenceTerms_nonnegative line 40