OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListScheduleOrder.lean
9 declarations, 0 contain sorry, 0 declared as axioms
Exact edge order in the emitted next-round list: retained edges followed by three consecutive edges for each selected source edge.
- abbrev
OAI.ContinuumCoulomb.QuantumListSchedule.Tagsline 12 - def
OAI.ContinuumCoulomb.QuantumListSchedule.tagValueline 15 - def
OAI.ContinuumCoulomb.QuantumListSchedule.flatTagEquivline 20 - theorem
OAI.ContinuumCoulomb.QuantumListSchedule.family_ofFnline 24 - theorem
OAI.ContinuumCoulomb.QuantumListSchedule.ofFn_triplesline 33 - theorem
OAI.ContinuumCoulomb.QuantumListSchedule.value_ofFnline 48 - theorem
OAI.ContinuumCoulomb.QuantumListSchedule.value_lengthline 67 - def
OAI.ContinuumCoulomb.QuantumListSchedule.tagEquivline 72 - theorem
OAI.ContinuumCoulomb.QuantumListSchedule.tagEquiv_getline 75