OAI/Algebra/AuslanderReiten/Coordinates/FiniteConnectingProducts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.FiniteLeftModule.resolutionSourceAtStableEquiv line 18
2. theorem OAI.ArExplicit.FiniteLeftModule.resolutionSourceAtStableEquiv_mk line 28
3. theorem OAI.ArExplicit.FiniteLeftModule.resolutionSourceAtStableEquiv_postcomp line 36
4. theorem OAI.ArExplicit.FiniteLeftModule.resolutionSourceAtStableEquiv_identity line 50
5. theorem OAI.ArExplicit.FiniteLeftModule.resolutionConnecting_product_source line 67