OAI/GroupTheory/PolycyclicRecognition/Algebra/PolycyclicTorsionFree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Torsion-free finite-index subgroups of polycyclic groups

This proves the torsion-free consequence of Robinson, A Course in the Theory of Groups, second edition, Theorem 5.4.15(i), needed by the duality comparison. The proof is induction along the actual cyclic subnormal series.

  1. theorem OAI.PolycyclicRecognition.torsionFree_finiteIndex_of_equiv line 19
  2. theorem OAI.PolycyclicRecognition.torsionFree_finiteIndex_of_cyclicStep line 28
  3. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_torsionFree_finiteIndex line 40
  4. theorem OAI.PolycyclicRecognition.polycyclicTorsionFreeIndexInput line 63

    Source documentation

    Every polycyclic group has a torsion-free subgroup of finite index.

    theorem polycyclicTorsionFreeIndexInput : PolycyclicTorsionFreeIndexInput :=
…

    Mentions: OAI.PolycyclicRecognition.PolycyclicTorsionFreeIndexInput