OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentCentralRoots.lean

Isolated centers in torsion-free nilpotent groups

If a nonzero power of an element is central, its unipotent action on a maximal abelian normal subgroup has finite order and is trivial. The element belongs to that abelian subgroup, where torsion freeness makes roots unique. Thus it is central, and the quotient by the center is torsion free.