OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentIntrinsicIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent-source integration into any Lie group

Codimension-one induction uses the intrinsic adjoint exponential identity. The target has no representation hypothesis.

  1. theorem OAI.PolycyclicRecognition.integrate_polynomial_nilpotent line 24