feat: port Algebra.Category.Module.ChangeOfRings (#4300)

Co-authored-by: Calvin Lee <calvins.lee@utah.edu> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
leanprover-community · Jul 7, 2023 · caec998 · caec998
1 parent 811ee33
commit caec998
Show file tree

Hide file tree

Showing 2 changed files with 725 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -58,6 +58,7 @@ import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 import Mathlib.Algebra.Category.ModuleCat.Algebra
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Biproducts
+import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.FilteredColimits