OAI/Algebra/AuslanderReiten/Bar/BarBimodule.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.AbsoluteBar.Enveloping line 15
2. def OAI.ArExplicit.AbsoluteBar.representation line 17
3. def OAI.ArExplicit.AbsoluteBar.bimodule line 24
4. def OAI.ArExplicit.AbsoluteBar.moduleObject line 27
5. instance OAI.ArExplicit.AbsoluteBar.baseModule line 31
6. instance OAI.ArExplicit.AbsoluteBar.bimoduleTower line 34
7. theorem OAI.ArExplicit.AbsoluteBar.bimodule_smul_tmul line 40
8. def OAI.ArExplicit.AbsoluteBar.differential line 43
9. theorem OAI.ArExplicit.AbsoluteBar.differential_apply line 56
10. def OAI.ArExplicit.AbsoluteBar.complex line 61
11. theorem OAI.ArExplicit.AbsoluteBar.differential_exact line 70