OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothExponentialCurve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth one-parameter curves of the intrinsic exponential

  1. theorem OAI.PolycyclicRecognition.contMDiff_invariantVectorField_infty line 17
  2. theorem OAI.PolycyclicRecognition.IsGroupExponential.contMDiff_curve line 45