OAI/GroupTheory/PolycyclicRecognition/Geometry/DerivationLieSpace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual tangent algebra of the derivation extension

The type synonym keeps exponential group coordinates distinct from the raw semidirect group on the product vector space.

  1. def OAI.PolycyclicRecognition.DerivationLieSpace line 19
  2. instance OAI.PolycyclicRecognition.derivationLieSpaceRealNormed line 22
  3. instance OAI.PolycyclicRecognition.derivationLieSpaceFiniteDimensional line 34
  4. def OAI.PolycyclicRecognition.derivationLieSpaceSplit line 39
  5. theorem OAI.PolycyclicRecognition.derivationLieSpace_nilpotent line 42
  6. def OAI.PolycyclicRecognition.derivationNilpotentLieModel line 47