OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentUniqueRoots.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unique roots in torsion-free nilpotent groups

Induction through the torsion-free center quotient reduces equality of powers to a central difference. The two elements then commute, and torsion freeness kills that difference.

  1. theorem OAI.PolycyclicRecognition.nilpotent_isMulTorsionFree line 16