OAI/GroupTheory/PolycyclicRecognition/Algebra/PolyZExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extending a torsion-free cyclic series by one cyclic quotient

  1. theorem OAI.PolycyclicRecognition.cyclicStep_factorMap_injective line 13
  2. theorem OAI.PolycyclicRecognition.TorsionFreeCyclicFactors.map line 36
  3. def OAI.PolycyclicRecognition.cyclicSeriesSnoc line 48
  4. theorem OAI.PolycyclicRecognition.cyclicStep_torsionFree_congr line 61
  5. theorem OAI.PolycyclicRecognition.TorsionFreeCyclicFactors.snoc line 69
  6. theorem OAI.PolycyclicRecognition.isPolyZ_of_normal_cyclic_quotient line 90