OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialCentralLayerUnipotence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth forces unipotent powers on central layers

  1. theorem OAI.PolycyclicRecognition.upperCentralLayerMap_surjective line 16
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_centralLayer_unipotent_power line 30