OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentFaithfulIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent-source integration into a faithfully represented Lie group

The proof uses codimension-one induction. The representation of the target need not be unipotent; it identifies conjugation along the complementary one-parameter subgroup. The source model is constructed unconditionally.

  1. theorem OAI.PolycyclicRecognition.integrate_polynomial_nilpotent_to_faithful line 26