OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentModelIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating a given nilpotent model into any Lie group

The now-proved nilpotent-model comparison transports the source to the constructed coordinate model. Intrinsic integration then reaches the target.

  1. theorem OAI.PolycyclicRecognition.nilpotentSmoothIntegrationInput line 22