OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteProductGlobalChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global exponential charts from one finite product formula

The polynomial degree can be any finite common bound supplied by a concrete representation. It need not already equal the Lie nilpotency class.

  1. theorem OAI.PolycyclicRecognition.globalExponentialChart_of_finite_products line 21