OAI/Algebra/AuslanderReiten/Modules/FiniteModuleNaturality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.FiniteLeftModule.resolutionCokernelMap_comp line 17
2. theorem OAI.ArExplicit.FiniteLeftModule.resolutionMap_id line 24
3. theorem OAI.ArExplicit.FiniteLeftModule.resolutionMap_comp line 36
4. theorem OAI.ArExplicit.FiniteLeftModule.resolutionMap_surjective line 46
5. def OAI.ArExplicit.FiniteLeftModule.resolutionTriangle line 68
6. theorem OAI.ArExplicit.FiniteLeftModule.resolutionTriangle_distinguished line 77
7. theorem OAI.ArExplicit.FiniteLeftModule.resolutionTriangle_first line 84
8. theorem OAI.ArExplicit.FiniteLeftModule.resolutionTriangle_second line 88
9. abbrev OAI.ArExplicit.FiniteLeftModule.resolutionConnecting line 95
10. theorem OAI.ArExplicit.FiniteLeftModule.resolutionConnecting_natural line 108