OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumScalarReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact reindexing of the four-rational local-core sums. This lets the literal support-list coordinates evaluate the propagation Gram matrix.

  1. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.scalar_add_eq line 13
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.scalar_sum_eq line 14
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.scalar_finiteSum_eq line 20
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.scalar_finiteSum_reindex line 26
  5. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.reindex line 32
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.matMul_reindex line 35
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.adjoint_reindex line 41
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.gram_reindex line 44