OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexDiagonalCycles.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Cycles and the leading component of a total boundary

  1. def OAI.PolycyclicRecognition.IsDiagonalCycle line 15
  2. theorem OAI.PolycyclicRecognition.diagonalBoundary_isCycle line 22
  3. theorem OAI.PolycyclicRecognition.IsDiagonalCycle.sub line 31
  4. theorem OAI.PolycyclicRecognition.diagonalBoundary_single_above line 44
  5. theorem OAI.PolycyclicRecognition.diagonalBoundary_single_leading line 61
  6. theorem OAI.PolycyclicRecognition.row_cycle_lift_of_exactAt line 73
  7. theorem OAI.PolycyclicRecognition.row_cycle_lift line 85