OAI/Algebra/AuslanderReiten/Resolutions/FiniteResolutionProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.FiniteLeftModule.homotopyResolutionMap_add line 16
  2. theorem OAI.ArExplicit.FiniteLeftModule.homotopyResolutionMap_zero line 23
  3. def OAI.ArExplicit.FiniteLeftModule.pairFst line 31
  4. def OAI.ArExplicit.FiniteLeftModule.pairSnd line 32
  5. def OAI.ArExplicit.FiniteLeftModule.pairInl line 33
  6. def OAI.ArExplicit.FiniteLeftModule.pairInr line 34
  7. abbrev OAI.ArExplicit.FiniteLeftModule.resolutionPairBicone line 36
  8. theorem OAI.ArExplicit.FiniteLeftModule.resolutionPairBicone_total line 56
  9. def OAI.ArExplicit.FiniteLeftModule.resolutionPairBilimit line 69
  10. instance OAI.ArExplicit.FiniteLeftModule.resolutionPairHasBiproduct line 72
  11. def OAI.ArExplicit.FiniteLeftModule.resolutionPairIso line 76
  12. theorem OAI.ArExplicit.FiniteLeftModule.resolutionPairIso_hom_fst line 80
  13. theorem OAI.ArExplicit.FiniteLeftModule.resolutionPairIso_hom_snd line 85