OAI/Algebra/AuslanderReiten/Evaluation/ConcreteEvaluatedBase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.T.simpleEvaluationFunctor line 17
  2. abbrev OAI.ArExplicit.T.simpleOrdinaryResolution line 20
  3. abbrev OAI.ArExplicit.T.shuffledBarComplex line 24
  4. def OAI.ArExplicit.T.ordinaryBarTermIso line 29
  5. theorem OAI.ArExplicit.T.ordinaryBarTermIso_d line 31
  6. def OAI.ArExplicit.T.simpleOrdinaryBarIso line 37
  7. def OAI.ArExplicit.T.ordinaryFirstHom line 42
  8. def OAI.ArExplicit.T.ordinarySecondHom line 45
  9. theorem OAI.ArExplicit.T.simpleOrdinaryBarIso_first line 48
  10. theorem OAI.ArExplicit.T.simpleOrdinaryBarIso_second line 59