OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialUnipotentModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unipotent realization of a polynomial exponential model

This construction is internal to the given polynomial model. It does not assert the finite BCH formula for an arbitrary Lie group.

  1. theorem OAI.PolycyclicRecognition.exists_polynomial_unipotent_model line 23