OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvablePolynomialGrowthPolycyclic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth forces polycyclicity in a solvable group

Induct on the integer growth degree. A virtual quotient to the integers gives a finitely generated solvable kernel with strictly lower degree. Its cyclic extension is polycyclic, and the final finite solvable extension is polycyclic.

  1. theorem OAI.PolycyclicRecognition.solvable_polynomial_growth_polycyclic_degree line 19
  2. theorem OAI.PolycyclicRecognition.solvable_polynomial_growth_polycyclic line 54
  3. theorem OAI.PolycyclicRecognition.virtually_solvable_polynomial_growth_virtually_polycyclic line 63