OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRationalCrossing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A simultaneous crossing-removal layer as exact rational ordinary-spin data.

  1. structure OAI.ContinuumCoulomb.QMARationalCrossingLayer line 13
  2. def OAI.ContinuumCoulomb.QMARationalCrossingLayer.source line 23
  3. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.source_matrix line 38
  4. def OAI.ContinuumCoulomb.QMARationalCrossingLayer.scale line 60
  5. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.scale_cast line 66
  6. def OAI.ContinuumCoulomb.QMARationalCrossingLayer.output line 75
  7. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_matrix line 89
  8. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_energy_error line 104
  9. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_edge_count line 112