OAI/GroupTheory/PolycyclicRecognition/Algebra/SingleRowsTotal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Totalization of a bicomplex supported in row zero

  1. abbrev OAI.PolycyclicRecognition.singleRowsBicomplex line 13
  2. abbrev OAI.PolycyclicRecognition.diagonalZeroIndex line 16
  3. def OAI.PolycyclicRecognition.singleRowsTotalTo line 19
  4. def OAI.PolycyclicRecognition.singleRowsTotalFrom line 23
  5. theorem OAI.PolycyclicRecognition.singleRowsTotal_to_from line 27
  6. theorem OAI.PolycyclicRecognition.singleRowsTotal_from_to line 34
  7. def OAI.PolycyclicRecognition.singleRowsTotalEquiv line 58
  8. theorem OAI.PolycyclicRecognition.singleRowsTotal_d line 64
  9. def OAI.PolycyclicRecognition.singleRowsTotalIso line 83