OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothExponentialDifferential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The derivative of a smooth intrinsic exponential at zero

  1. theorem OAI.PolycyclicRecognition.hasMFDerivAt_zero_of_smooth_linear_curves line 20
  2. theorem OAI.PolycyclicRecognition.IsGroupExponential.hasMFDerivAt_zero_of_smooth line 47