OAI/Algebra/AuslanderReiten/Bar/BarSuffix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.AbsoluteBar.suffixComparison line 12
2. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_succ_tmul line 16
3. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_left line 20
4. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_right line 28
5. def OAI.ArExplicit.AbsoluteBar.suffixComparisonMap line 42
6. theorem OAI.ArExplicit.AbsoluteBar.double_zero line 49

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

7. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_boundary_zero line 53
8. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_boundary line 73
9. theorem OAI.ArExplicit.AbsoluteBar.suffixComparison_augmentation line 90