OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentUpperCentralRoots.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Torsion-free upper central quotients

Each upper central term is closed under taking roots. The center of every resulting quotient therefore embeds faithfully into a finite-dimensional rational space whenever the original group has finite integral dimension.

  1. theorem OAI.PolycyclicRecognition.quotient_torsionFree_of_root_closed line 19
  2. theorem OAI.PolycyclicRecognition.nilpotent_upperCentralQuotient_torsionFree line 30
  3. theorem OAI.PolycyclicRecognition.nilpotent_upperCentral_center_rational_finite line 54