OAI/Analysis/HardSphere/Geometry/RealComp.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HardSphere.SmoothMultiplier.realCompline 20 - lemma
OAI.HardSphere.SmoothMultiplier.partial_realCompline 25