OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianByFiniteContractor.lean

The finiteness endgame from one contracting element

For a nilpotent-by-abelian-by-finite group it suffices to find any contracting element on the nilpotent abelianization. A positive power enters the abelian normal subgroup of the quotient; finite conjugation averaging then supplies the central contractor needed for the finiteness argument.