OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListScheduleRelabel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The emitted schedule has exactly the canonical subdivided coordinates, up to its explicit finite vertex and edge permutations.

  1. def OAI.ContinuumCoulomb.QuantumListSchedule.iterateRelabel line 13
  2. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterateRelabel_geometry line 20