OAI/Geometry/WeakHessian/Calculus/CompactHopfCurve.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessianTransport.compactHopf_uniform_dataline 21 - lemma
OAI.WeakHessianTransport.compactHopf_exists_L2_curveline 53