OAI/Algebra/AuslanderReiten/Tensor/TwistedTensorResolution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.T.sourceTwist line 21
  2. def OAI.ArExplicit.T.twistedTensorBarResolution line 24
  3. abbrev OAI.ArExplicit.T.productSourceData line 35
  4. abbrev OAI.ArExplicit.T.sourceData line 45
  5. def OAI.ArExplicit.T.sourceFourthEquiv line 48
  6. theorem OAI.ArExplicit.T.source_exact line 51
  7. def OAI.ArExplicit.T.sourceProductBaseTyped line 60
  8. def OAI.ArExplicit.T.sourceQuotientRestriction line 66
  9. def OAI.ArExplicit.T.sourceProductBaseRestricted line 75
  10. def OAI.ArExplicit.T.sourceToTwistedRegular line 78
  11. def OAI.ArExplicit.T.sourceBaseEquiv line 81
  12. theorem OAI.ArExplicit.T.source_product_finite line 87
  13. theorem OAI.ArExplicit.T.source_product_projective line 96
  14. theorem OAI.ArExplicit.T.source_finite line 108
  15. theorem OAI.ArExplicit.T.source_projective line 115