OAI/Algebra/AuslanderReiten/Complete/CompleteShiftDual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.HomExactAt.congr line 20
  2. theorem OAI.ArExplicit.HomExactAt.of_shortComplex_iso line 37
  3. def OAI.ArExplicit.CompleteComparison.reverseShortComplexIso line 48
  4. def OAI.ArExplicit.DualExactCochain line 68
  5. theorem OAI.ArExplicit.DualExactCochain.of_chain line 75
  6. theorem OAI.ArExplicit.DualExactCochain.to_chain line 82
  7. theorem OAI.ArExplicit.DualExactCochain.shift line 91
  8. structure OAI.ArExplicit.TotallyAcyclicCochain line 100
  9. theorem OAI.ArExplicit.TotallyAcyclicCochain.of_chain line 108
  10. theorem OAI.ArExplicit.TotallyAcyclicCochain.to_chain line 113
  11. theorem OAI.ArExplicit.TotallyAcyclicCochain.shift line 118
  12. theorem OAI.ArExplicit.TotallyAcyclicComplex.cochainShift line 129