OAI/GroupTheory/PolycyclicRecognition/Algebra/PolycyclicPolynomialNilpotence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth of virtually polycyclic groups

Polynomial growth forces virtual nilpotence. The finite-index passage to finite integral dimension and the central-layer argument are both proved; no Milnor--Wolf conclusion is assumed here.

  1. theorem OAI.PolycyclicRecognition.polycyclic_polynomial_growth_virtually_nilpotent line 21
  2. theorem OAI.PolycyclicRecognition.virtually_polycyclic_polynomial_growth_virtually_nilpotent line 38
  3. theorem OAI.PolycyclicRecognition.virtually_solvable_polynomial_growth_virtually_nilpotent line 53