OAI/Algebra/AuslanderReiten/Modules/FiniteModuleEvaluation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.FiniteLeftModule.evaluated line 18
  2. def OAI.ArExplicit.FiniteLeftModule.evaluationMap line 26
  3. theorem OAI.ArExplicit.FiniteLeftModule.evaluationMap_id line 31
  4. theorem OAI.ArExplicit.FiniteLeftModule.evaluationMap_comp line 35
  5. def OAI.ArExplicit.FiniteLeftModule.evaluationStableIso line 40
  6. theorem OAI.ArExplicit.FiniteLeftModule.evaluated_projective line 52
  7. theorem OAI.ArExplicit.FiniteLeftModule.evaluation_shortExact line 65
  8. def OAI.ArExplicit.FiniteLeftModule.evaluationTriangle line 81
  9. theorem OAI.ArExplicit.FiniteLeftModule.evaluationTriangle_distinguished line 86
  10. def OAI.ArExplicit.FiniteLeftModule.evaluationSuccessorIso line 90
  11. theorem OAI.ArExplicit.FiniteLeftModule.evaluationSuccessorIso_hom line 99
  12. theorem OAI.ArExplicit.FiniteLeftModule.evaluationConnecting_natural line 119