OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialModelDynkin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The precise finite BCH input for polynomial coordinate models

The faithful representation gives a finite product formula at a concrete operator bound. Coefficient stability and vanishing of long brackets reduce it to every supplied lower-central-series bound.

  1. theorem OAI.PolycyclicRecognition.polynomialCoordinate_product_of_class line 24
  2. theorem OAI.PolycyclicRecognition.nilpotentDynkinExpansionInput_polynomial line 34