OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPauliSubdivision.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A simultaneous real subdivision step for bounded-support even-Y words.
- theorem
OAI.ContinuumCoulomb.qmaPauliSubdivision_existsline 13