OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianCyclicPolynomialNilpotence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-growth cyclic extensions of free abelian groups

The action has a unipotent positive power. Its powered semidirect product is nilpotent and embeds as an actual subgroup of finite index in the given group.

  1. def OAI.PolycyclicRecognition.cyclicSemidirectKernelEquiv line 19
  2. theorem OAI.PolycyclicRecognition.semidirect_abelian_nilpotent_of_unipotent line 35
  3. theorem OAI.PolycyclicRecognition.abelian_cyclic_polynomial_growth_virtually_nilpotent line 62