OAI/Algebra/AuslanderReiten/Cones/TwoConeBoundaryIdentification.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.TwoCone.middleTermModule line 18
2. def OAI.ArExplicit.TwoCone.middleCoverQuotient line 24
3. theorem OAI.ArExplicit.TwoCone.middleCoverQuotient_surjective line 28
4. theorem OAI.ArExplicit.TwoCone.middleStepInclusion_injective line 34
5. theorem OAI.ArExplicit.TwoCone.middleStep_exact line 39
6. def OAI.ArExplicit.TwoCone.middleSuccessorShiftIso line 51
7. abbrev OAI.ArExplicit.TwoCone.skeletonConnecting line 62
8. abbrev OAI.ArExplicit.TwoCone.topConnecting line 70
9. theorem OAI.ArExplicit.TwoCone.skeletonConnecting_eq line 78
10. theorem OAI.ArExplicit.TwoCone.topConnecting_eq line 102