OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexTotalExact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exactness of first-quadrant total complexes with exact rows

  1. theorem OAI.PolycyclicRecognition.totalCycle_toDiagonal line 15
  2. theorem OAI.PolycyclicRecognition.bicomplex_total_cycle_boundary_of_exact_diagonal line 33
  3. theorem OAI.PolycyclicRecognition.bicomplex_total_exactAt_of_exact_diagonal line 44
  4. theorem OAI.PolycyclicRecognition.bicomplex_total_cycle_boundary line 58
  5. theorem OAI.PolycyclicRecognition.bicomplex_total_exactAt line 65
  6. theorem OAI.PolycyclicRecognition.bicomplex_total_homology_isZero_of_diagonal line 69
  7. theorem OAI.PolycyclicRecognition.bicomplex_total_homology_isZero line 75