OAI/Algebra/AuslanderReiten/Bar/ModuleBarCochain.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ModuleBar.suffix3 line 14
  2. theorem OAI.ArExplicit.ModuleBar.suffix3_tmul line 47
  3. def OAI.ArExplicit.ModuleBar.cochain3Linear line 50
  4. theorem OAI.ArExplicit.ModuleBar.cochain3Linear_tmul line 53
  5. theorem OAI.ArExplicit.ModuleBar.cochain3Linear_left line 59
  6. def OAI.ArExplicit.ModuleBar.cochain3 line 65
  7. theorem OAI.ArExplicit.ModuleBar.cochain3_boundary_tmul line 70
  8. theorem OAI.ArExplicit.ModuleBar.cochain3_closed line 82
  9. theorem OAI.ArExplicit.ModuleBar.cochain3_cycle line 92
  10. def OAI.ArExplicit.ModuleBar.extClass3 line 101
  11. theorem OAI.ArExplicit.ModuleBar.extClass3_eq_zero_iff line 107
  12. theorem OAI.ArExplicit.ModuleBar.extClass3_ne_zero_of_detector line 126