OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentRootGenerators.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finitely generated subgroup containing a power of every element

Central-quotient induction uses the uniform abelian rank bound in all quotients. The chosen subgroup is an actual finite generating core; the statement does not assert finite generation of the original nilpotent group.

  1. theorem OAI.PolycyclicRecognition.nilpotent_quotient_exists_fg_subgroup_containing_powers line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_exists_fg_subgroup_containing_powers line 41