OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrdinalPlacement.lean
4 declarations, 0 contain sorry, 0 declared as axioms
Apply explicit ordinal ranks to the cell-slot interface used by geometry.
- theorem
OAI.ContinuumCoulomb.QuantumOrdinalPlacement.coordinates_eqline 11 - def
OAI.ContinuumCoulomb.QuantumOrdinalPlacement.coordinatesline 18 - theorem
OAI.ContinuumCoulomb.QuantumOrdinalPlacement.fiber_cardline 21 - def
OAI.ContinuumCoulomb.QuantumOrdinalPlacement.slotsline 29