OAI/Geometry/SmoothYau/Estimates/RectangularFactorization.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.YauCounterexamples.rectangular_factorizationline 11 - theorem
OAI.YauCounterexamples.local_factor_of_kernelline 39