feat: port Algebra.Category.Module.Basic (#3260)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · Apr 11, 2023 · f5a903b · f5a903b
1 parent 814b0c4
commit f5a903b
Show file tree

Hide file tree

Showing 2 changed files with 394 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -32,6 +32,7 @@ import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.Category.GroupCat.Basic
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.Algebra.Category.GroupCat.Zero
+import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic