OAI/Algebra/AuslanderReiten/Bar/ModuleBarSuffix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ModuleBar.suffixComparison line 13
2. theorem OAI.ArExplicit.ModuleBar.suffixComparison_succ_tmul line 17
3. theorem OAI.ArExplicit.ModuleBar.suffixComparison_left line 21
4. def OAI.ArExplicit.ModuleBar.suffixComparisonMap line 29
5. theorem OAI.ArExplicit.ModuleBar.double_zero line 36

   Also declared: OAI/Algebra/AuslanderReiten/Bar/ModuleBar.lean:104 (same declaration text).

6. theorem OAI.ArExplicit.ModuleBar.suffixComparison_boundary_zero line 40
7. theorem OAI.ArExplicit.ModuleBar.suffixComparison_boundary line 60
8. theorem OAI.ArExplicit.ModuleBar.suffixComparison_augmentation line 77