OAI/GroupTheory/PolycyclicRecognition/Geometry/LinearExponentialAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The real action generated by an arbitrary linear logarithm

No nilpotence of the logarithm is needed. The operator exponential gives an actual smooth action on the additive vector model.

  1. def OAI.PolycyclicRecognition.additiveOperatorUnitAut line 17
  2. def OAI.PolycyclicRecognition.additiveOperatorUnitAutHom line 33
  3. def OAI.PolycyclicRecognition.linearExponentialUnits line 39
  4. def OAI.PolycyclicRecognition.linearExponentialAction line 51
  5. theorem OAI.PolycyclicRecognition.linearExponentialAction_apply line 55
  6. theorem OAI.PolycyclicRecognition.linearExponentialAction_smooth line 60