OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthNilpotentCentralLayers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-index nilpotence from the central layers

For a polycyclic solvable group of finite integral dimension, polynomial growth forces unipotent action on every central layer of its maximal nilpotent normal subgroup. A finite intersection of the resulting normal subgroups acts nilpotently on all layers and is itself nilpotent.

  1. theorem OAI.PolycyclicRecognition.centralLayer_finite_free line 22
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_nilpotent_finiteIndex_of_finiteDimension line 42