OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianKernelPolynomialNilpotence.lean

Polynomial growth with an abelian kernel and cyclic quotient

The kernel need not be torsion free or initially finitely generated. Polynomial growth supplies finite generation. A characteristic finite-index torsion-free subgroup gives an actual finite-index cyclic extension, where the integral-action argument applies.