OAI/GroupTheory/PolycyclicRecognition/Algebra/SequentialModuleTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Removing the first stage of a sequential integral module colimit

  1. abbrev OAI.PolycyclicRecognition.moduleTailMap line 13
  2. instance OAI.PolycyclicRecognition.moduleTailMap_directed line 16
  3. abbrev OAI.PolycyclicRecognition.ModuleTailLimit line 24
  4. def OAI.PolycyclicRecognition.moduleTailToOriginal line 26
  5. theorem OAI.PolycyclicRecognition.moduleTailToOriginal_of line 33
  6. def OAI.PolycyclicRecognition.moduleOriginalToTail line 38
  7. theorem OAI.PolycyclicRecognition.moduleOriginalToTail_of line 54
  8. theorem OAI.PolycyclicRecognition.moduleTail_original_inverse line 59
  9. theorem OAI.PolycyclicRecognition.moduleOriginal_tail_inverse line 69
  10. def OAI.PolycyclicRecognition.sequentialModuleTailEquiv line 80