OAI/GroupTheory/PolycyclicRecognition/Algebra/PolyZComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The virtual poly-Z refinement of a polycyclic series

  1. theorem OAI.PolycyclicRecognition.polyZ_finiteIndex_of_equiv line 13
  2. theorem OAI.PolycyclicRecognition.polyZ_finiteIndex_of_cyclicStep line 22
  3. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_polyZ_finiteIndex line 34