OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentIntegrationConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integration between the nilpotent models used by the application

Global exponential coordinates and one application of the finite Dynkin identity to the product construct the homomorphism. Its smoothness and actual differential are proved by exponential curves. The target is explicitly nilpotent; integration into the ambient solvable group remains a separate input.

  1. theorem OAI.PolycyclicRecognition.nilpotentSmoothIntegration_of_coordinates line 33