OAI/Algebra/AuslanderReiten/Bar/BarComplex.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.AbsoluteBar.object line 14
  2. def OAI.ArExplicit.AbsoluteBar.left line 18
  3. def OAI.ArExplicit.AbsoluteBar.right line 22
  4. theorem OAI.ArExplicit.AbsoluteBar.left_zero line 26
  5. theorem OAI.ArExplicit.AbsoluteBar.right_zero line 27
  6. theorem OAI.ArExplicit.AbsoluteBar.left_tmul line 28
  7. theorem OAI.ArExplicit.AbsoluteBar.right_tmul line 30
  8. theorem OAI.ArExplicit.AbsoluteBar.left_one line 33
  9. theorem OAI.ArExplicit.AbsoluteBar.left_mul line 37
  10. theorem OAI.ArExplicit.AbsoluteBar.left_right line 42
  11. def OAI.ArExplicit.AbsoluteBar.boundary line 51
  12. theorem OAI.ArExplicit.AbsoluteBar.boundary_zero_tmul line 55
  13. theorem OAI.ArExplicit.AbsoluteBar.boundary_succ_tmul line 56
  14. theorem OAI.ArExplicit.AbsoluteBar.boundary_left line 60
  15. theorem OAI.ArExplicit.AbsoluteBar.boundary_right line 70
  16. theorem OAI.ArExplicit.AbsoluteBar.double_zero line 85

    Also declared: OAI/Algebra/AuslanderReiten/Bar/BarCasimir.lean:75 (same declaration text), OAI/Algebra/AuslanderReiten/Bar/BarSuffix.lean:49 (same declaration text).

  17. theorem OAI.ArExplicit.AbsoluteBar.boundary_squared line 89
  18. def OAI.ArExplicit.AbsoluteBar.contraction line 106
  19. theorem OAI.ArExplicit.AbsoluteBar.contraction_identity line 109
  20. theorem OAI.ArExplicit.AbsoluteBar.augmentation_contraction line 118
  21. theorem OAI.ArExplicit.AbsoluteBar.boundary_exact line 121