OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentSemidirectGroup.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Analytic semidirect products for the nilpotent induction

The carrier is the vector space L × ℝ. Its operations are polynomial because the action is the exponential of a nilpotent derivation.

  1. def OAI.PolycyclicRecognition.derivationSemidirectEquiv line 22
  2. def OAI.PolycyclicRecognition.derivationSemidirectGroup line 29
  3. theorem OAI.PolycyclicRecognition.derivationSemidirect_mul line 34
  4. theorem OAI.PolycyclicRecognition.derivationSemidirect_one line 38
  5. theorem OAI.PolycyclicRecognition.derivationSemidirect_inv line 43
  6. theorem OAI.PolycyclicRecognition.contDiff_derivationSemidirect_mul line 49
  7. theorem OAI.PolycyclicRecognition.contDiff_derivationSemidirect_inv line 62
  8. theorem OAI.PolycyclicRecognition.derivationSemidirectLieGroup line 68