OAI/Algebra/AuslanderReiten/Triangular/TriangularCategory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.TriangularInduction.eFunctor line 22
2. def OAI.ArExplicit.TriangularInduction.jFunctor line 28
3. instance OAI.ArExplicit.TriangularInduction.(instance at line 34) line 34
4. instance OAI.ArExplicit.TriangularInduction.(instance at line 42) line 42
5. instance OAI.ArExplicit.TriangularInduction.(instance at line 50) line 50
6. instance OAI.ArExplicit.TriangularInduction.(instance at line 59) line 59
7. instance OAI.ArExplicit.TriangularInduction.(instance at line 68) line 68
8. instance OAI.ArExplicit.TriangularInduction.(instance at line 75) line 75
9. theorem OAI.ArExplicit.TriangularInduction.eToJCochain_eq_zero line 82