OAI/Algebra/AuslanderReiten/Evaluation/EvaluatedMiddleShift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.T.evaluatedSimpleObject line 23
  2. abbrev OAI.ArExplicit.T.evaluatedSingletonModule line 26
  3. abbrev OAI.ArExplicit.T.evaluatedSingletonResolution line 28
  4. def OAI.ArExplicit.T.evaluatedSingletonPairEquiv line 31
  5. def OAI.ArExplicit.T.evaluatedSingletonProductIso line 37
  6. def OAI.ArExplicit.T.evaluatedSingletonFst line 43
  7. def OAI.ArExplicit.T.evaluatedSingletonSnd line 47
  8. theorem OAI.ArExplicit.T.evaluatedSingletonProductIso_fst line 51
  9. theorem OAI.ArExplicit.T.evaluatedSingletonProductIso_snd line 58
  10. def OAI.ArExplicit.T.evaluatedBaseFullHomEquiv line 65
  11. def OAI.ArExplicit.T.evaluatedSingletonHomEquiv line 71
  12. def OAI.ArExplicit.T.evaluatedSingletonFullHomEquiv line 80