OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothExponentialHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of a height specified on exponential curves

  1. theorem OAI.PolycyclicRecognition.contMDiff_height_of_exponential_linear line 18