OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompleteCohomologyLongExact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exactness at the completed connecting maps

  1. theorem OAI.PolycyclicRecognition.shiftedCompleteCohomology_boundary_exact line 12
  2. theorem OAI.PolycyclicRecognition.presentationKernelMap_normalized_stable line 39
  3. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_rotation line 56
  4. theorem OAI.PolycyclicRecognition.rotation_complete_retract line 90
  5. theorem OAI.PolycyclicRecognition.rotation_complete_inclusion_zero line 99
  6. theorem OAI.PolycyclicRecognition.shiftedCompleteCohomology_map_boundary_exact line 112