OAI/Algebra/AuslanderReiten/Triangular/TriangularHom.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TriangularModule.hom line 18
  2. theorem OAI.ArExplicit.TriangularModule.hom_top line 28
  3. theorem OAI.ArExplicit.TriangularModule.hom_bottom line 32
  4. theorem OAI.ArExplicit.TriangularModule.top_of_map line 38
  5. theorem OAI.ArExplicit.TriangularModule.bottom_of_map line 45
  6. def OAI.ArExplicit.TriangularModule.topMap line 52
  7. def OAI.ArExplicit.TriangularModule.bottomMap line 68
  8. theorem OAI.ArExplicit.TriangularModule.topMap_apply line 84
  9. theorem OAI.ArExplicit.TriangularModule.bottomMap_apply line 85
  10. theorem OAI.ArExplicit.TriangularModule.compatibility line 87
  11. theorem OAI.ArExplicit.TriangularModule.hom_topMap_bottomMap line 97
  12. theorem OAI.ArExplicit.TriangularModule.hom_ext line 104