OAI/Algebra/AuslanderReiten/Bar/BarCochain.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.AbsoluteBar.Cochain3 line 14
  2. def OAI.ArExplicit.AbsoluteBar.suffix3 line 16
  3. theorem OAI.ArExplicit.AbsoluteBar.suffix3_tmul line 49
  4. def OAI.ArExplicit.AbsoluteBar.cochain3Linear line 52
  5. theorem OAI.ArExplicit.AbsoluteBar.cochain3Linear_tmul line 55
  6. def OAI.ArExplicit.AbsoluteBar.bimoduleMap line 61
  7. theorem OAI.ArExplicit.AbsoluteBar.cochain3Linear_left line 76
  8. theorem OAI.ArExplicit.AbsoluteBar.suffix3_right line 82
  9. theorem OAI.ArExplicit.AbsoluteBar.cochain3Linear_right line 94
  10. def OAI.ArExplicit.AbsoluteBar.cochain3 line 104
  11. def OAI.ArExplicit.AbsoluteBar.IsCocycle3 line 107
  12. theorem OAI.ArExplicit.AbsoluteBar.cochain3_boundary_tmul line 111
  13. theorem OAI.ArExplicit.AbsoluteBar.cochain3_closed line 122
  14. theorem OAI.ArExplicit.AbsoluteBar.cochain3_cycle line 132
  15. def OAI.ArExplicit.AbsoluteBar.extClass3 line 141
  16. theorem OAI.ArExplicit.AbsoluteBar.extClass3_eq_zero_iff line 147