OAI/Algebra/AuslanderReiten/Cones/BimoduleTwoConeSides.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.T.productBaseTyped line 20
  2. def OAI.ArExplicit.T.baseQuotientRestriction line 26
  3. def OAI.ArExplicit.T.productBaseRestricted line 34
  4. def OAI.ArExplicit.T.baseToTensorRegular line 37
  5. def OAI.ArExplicit.T.bimoduleBaseCokernelEquiv line 39
  6. def OAI.ArExplicit.T.baseLeftEquiv line 42
  7. def OAI.ArExplicit.T.baseRightEquiv line 47
  8. theorem OAI.ArExplicit.T.baseTerm_left_projective line 52
  9. theorem OAI.ArExplicit.T.baseTerm_right_projective line 59
  10. theorem OAI.ArExplicit.T.firstTail_left_projective line 66
  11. theorem OAI.ArExplicit.T.firstTail_right_projective line 75
  12. theorem OAI.ArExplicit.T.firstTail_left_finite line 84
  13. theorem OAI.ArExplicit.T.firstTail_right_finite line 91