feat: port Algebra.Category.Ring.FilteredColimits (#4305)

leanprover-community · May 25, 2023 · 9a3eb6f · 9a3eb6f
1 parent 4c6c02a
commit 9a3eb6f
Show file tree

Hide file tree

Showing 2 changed files with 410 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -53,6 +53,7 @@ import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.Algebra.Category.MonCat.Limits
 import Mathlib.Algebra.Category.Ring.Basic
 import Mathlib.Algebra.Category.Ring.Colimits
+import Mathlib.Algebra.Category.Ring.FilteredColimits
 import Mathlib.Algebra.Category.Ring.Instances
 import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic