OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialProduct.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Products of exponential curves

Coordinates of the second kind require only smoothness of each individual one-parameter subgroup. Their differential at zero is the sum of the specified tangent vectors.

  1. def OAI.PolycyclicRecognition.exponentialProduct line 22
  2. def OAI.PolycyclicRecognition.tangentCombination line 27
  3. theorem OAI.PolycyclicRecognition.tangentCombination_apply line 31
  4. def OAI.PolycyclicRecognition.coordinateTail line 37
  5. theorem OAI.PolycyclicRecognition.coordinateTail_apply line 40
  6. theorem OAI.PolycyclicRecognition.tangentCombination_succ line 43
  7. theorem OAI.PolycyclicRecognition.IsGroupExponential.exponentialProduct_zero line 57
  8. theorem OAI.PolycyclicRecognition.IsGroupExponential.contMDiff_exponentialProduct line 68
  9. theorem OAI.PolycyclicRecognition.IsGroupExponential.hasMFDerivAt_exponentialProduct_zero line 80