OAI/GroupTheory/PolycyclicRecognition/Algebra/PolyZFiniteIndex.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-index poly-Z subgroups of polycyclic groups

  1. theorem OAI.PolycyclicRecognition.infiniteCyclic_torsionFree line 15
  2. theorem OAI.PolycyclicRecognition.polyZ_finiteIndex_of_cyclic_extension line 26