OAI/GroupTheory/PolycyclicRecognition/Algebra/UniversalCoefficientStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Independence of the low-degree universal BCH coefficients

Increasing the finite exponential and logarithm truncations changes only higher word degrees. Thus the universal coefficients can be restricted to the actual nilpotency class.

  1. theorem OAI.PolycyclicRecognition.rationalUniversalLogarithm_stable line 17
  2. theorem OAI.PolycyclicRecognition.universalLogarithmCoefficient_stable line 27
  3. theorem OAI.PolycyclicRecognition.universalDynkinCoefficients_stable line 37