OAI/Algebra/AuslanderReiten/Stable/StableExtEquiv.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.completeExtResolution line 16
  2. theorem OAI.ArExplicit.closed_of_indices line 18
  3. theorem OAI.ArExplicit.completeExtCycle_closed line 24
  4. def OAI.ArExplicit.completeExtCyclesMap line 33
  5. def OAI.ArExplicit.completeExtCyclesStable line 51
  6. theorem OAI.ArExplicit.completeExtCyclesMap_surjective line 54
  7. theorem OAI.ArExplicit.completeExtCyclesStable_surjective line 73
  8. theorem OAI.ArExplicit.completeExtCyclesStable_kernel line 77
  9. def OAI.ArExplicit.completeExtHomologyStableEquiv line 104
  10. def OAI.ArExplicit.positiveExtStableEquiv line 114
  11. theorem OAI.ArExplicit.positiveExtStableEquiv_extMk line 120