OAI/Algebra/AuslanderReiten/Triangular/TriangularFunctor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TriangularInduction.eMap line 19
  2. def OAI.ArExplicit.TriangularInduction.jMap line 21
  3. theorem OAI.ArExplicit.TriangularInduction.eMap_top line 24
  4. theorem OAI.ArExplicit.TriangularInduction.eMap_bottom line 28
  5. theorem OAI.ArExplicit.TriangularInduction.jMap_bottom line 34
  6. theorem OAI.ArExplicit.TriangularInduction.eMap_id line 37
  7. theorem OAI.ArExplicit.TriangularInduction.eMap_comp line 42
  8. theorem OAI.ArExplicit.TriangularInduction.jMap_id line 48
  9. theorem OAI.ArExplicit.TriangularInduction.jMap_comp line 54
  10. theorem OAI.ArExplicit.TriangularInduction.eMap_zero line 60
  11. theorem OAI.ArExplicit.TriangularInduction.jMap_zero line 66
  12. def OAI.ArExplicit.TriangularInduction.ePi line 73
  13. def OAI.ArExplicit.TriangularInduction.jPi line 88