feat: port Algebra.Category.ModuleCat.Adjunctions (#4457)

leanprover-community · May 30, 2023 · c57f43b · c57f43b
1 parent a206a3e
commit c57f43b
Show file tree

Hide file tree

Showing 2 changed files with 426 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -45,6 +45,7 @@ import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
 import Mathlib.Algebra.Category.GroupCat.Zero
 import Mathlib.Algebra.Category.GroupWithZeroCat
 import Mathlib.Algebra.Category.ModuleCat.Abelian
+import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Biproducts
 import Mathlib.Algebra.Category.ModuleCat.EpiMono