OAI/Algebra/AuslanderReiten/Cones/TwoConeModuleTriangles.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.TwoCone.termModule line 16
  2. abbrev OAI.ArExplicit.TwoCone.baseCokernelModule line 22
  3. abbrev OAI.ArExplicit.TwoCone.middleCokernelModule line 28
  4. abbrev OAI.ArExplicit.TwoCone.skeletonCokernelModule line 34
  5. abbrev OAI.ArExplicit.TwoCone.cokernelModule line 43
  6. theorem OAI.ArExplicit.TwoCone.exists_skeleton_triangle line 55
  7. theorem OAI.ArExplicit.TwoCone.exists_top_triangle line 74
  8. def OAI.ArExplicit.TwoCone.baseStepInclusion line 95
  9. theorem OAI.ArExplicit.TwoCone.baseStepInclusion_injective line 99
  10. theorem OAI.ArExplicit.TwoCone.baseStep_exact line 102
  11. def OAI.ArExplicit.TwoCone.baseSuccessorShiftIso line 112
  12. def OAI.ArExplicit.TwoCone.baseIteratedShiftIso line 122