OAI/Algebra/AuslanderReiten/Coordinates/TensorFiniteLift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.T.bimodule_term_finite_k line 18
  2. theorem OAI.ArExplicit.T.source_term_finite_k line 23
  3. abbrev OAI.ArExplicit.T.firstTailModule line 28
  4. def OAI.ArExplicit.T.sourceAugmentationEquiv line 31
  5. def OAI.ArExplicit.T.sourceFourthToTail line 36
  6. def OAI.ArExplicit.T.sourceShiftIso line 41
  7. def OAI.ArExplicit.T.finiteLift line 46
  8. def OAI.ArExplicit.T.finiteLiftClass line 53
  9. theorem OAI.ArExplicit.T.finiteLift_spec line 59
  10. theorem OAI.ArExplicit.T.firstTailModule_left_projective line 66
  11. theorem OAI.ArExplicit.T.firstTailModule_right_projective line 71
  12. theorem OAI.ArExplicit.T.firstTailModule_left_finite line 76
  13. theorem OAI.ArExplicit.T.firstTailModule_right_finite line 81