OAI/GroupTheory/PolycyclicRecognition/Geometry/AnalyticDerivationAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth real actions on polynomial exponential groups

Any derivation gives an action; nilpotence of the derivation is unnecessary.

  1. theorem OAI.PolycyclicRecognition.contDiff_analyticDerivationFlow line 16
  2. def OAI.PolycyclicRecognition.PolynomialExponentialCoordinates.analyticDerivationAction line 28
  3. theorem OAI.PolycyclicRecognition.PolynomialExponentialCoordinates.analyticDerivationAction_apply line 39
  4. theorem OAI.PolycyclicRecognition.PolynomialExponentialCoordinates.analyticDerivationAction_smooth line 43