OAI/Algebra/AuslanderReiten/Complete/ProjectiveCompleteResolution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.completeCochain_isZero_of_projectiveCokernel line 16
2. theorem OAI.ArExplicit.FiniteLeftModule.projective_completeCochain_isZero line 35
3. theorem OAI.ArExplicit.FiniteLeftModule.nonempty_projectiveMiddleShiftIso line 43
4. def OAI.ArExplicit.FiniteLeftModule.projectiveMiddleShiftIso line 55
5. theorem OAI.ArExplicit.FiniteLeftModule.projectiveMiddleShiftIso_hom line 67