OAI/Algebra/AuslanderReiten/HomComplex/FullHomProducts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.CompleteComparison.cocycleProduct line 17
  2. theorem OAI.ArExplicit.CompleteComparison.cocycleProduct_coe line 23
  3. def OAI.ArExplicit.CompleteComparison.shiftedCocycleHom line 26
  4. theorem OAI.ArExplicit.CompleteComparison.cocycleHom_component line 31
  5. theorem OAI.ArExplicit.CompleteComparison.cochain_component_transport line 38
  6. theorem OAI.ArExplicit.CompleteComparison.cocycleHom_product line 44
  7. theorem OAI.ArExplicit.CompleteComparison.cocycleProduct_respects_classes line 57
  8. def OAI.ArExplicit.CompleteComparison.fullHomProduct line 73
  9. theorem OAI.ArExplicit.CompleteComparison.fullHomProduct_mk line 80
  10. def OAI.ArExplicit.CompleteComparison.cocycleComparisonMap line 89
  11. theorem OAI.ArExplicit.CompleteComparison.fullHomStableEquiv_mk line 94
  12. theorem OAI.ArExplicit.CompleteComparison.fullHomStableEquiv_product line 100