OAI/Algebra/AuslanderReiten/Triangular/TriangularInduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.TriangularE line 13
2. abbrev OAI.ArExplicit.TriangularJ line 17
3. def OAI.ArExplicit.TriangularInduction.eHom line 27
4. def OAI.ArExplicit.TriangularInduction.jHom line 31
5. theorem OAI.ArExplicit.TriangularInduction.eHom_topMap line 35
6. theorem OAI.ArExplicit.TriangularInduction.jHom_bottomMap line 45
7. def OAI.ArExplicit.TriangularInduction.eHomEquiv line 58
8. def OAI.ArExplicit.TriangularInduction.jHomEquiv line 68
9. theorem OAI.ArExplicit.TriangularInduction.hom_E_J_eq_zero line 78