OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothRealActionModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A solvable Lie model for a smooth real action

The action may have expanding, contracting, or rotational parts. The model construction needs its actual smooth action, not a nilpotence assumption.

  1. def OAI.PolycyclicRecognition.realActionSemidirectEquiv line 21
  2. def OAI.PolycyclicRecognition.realActionSemidirectGroup line 27
  3. theorem OAI.PolycyclicRecognition.realActionSemidirectLieGroup line 33
  4. def OAI.PolycyclicRecognition.smoothRealActionModel line 58
  5. def OAI.PolycyclicRecognition.smoothRealActionModelEquiv line 73
  6. theorem OAI.PolycyclicRecognition.smoothRealActionModelEquiv_continuous line 79
  7. theorem OAI.PolycyclicRecognition.smoothRealActionModelEquiv_symm_continuous line 84