feat: port CategoryTheory.Localization.Construction (#2917)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
leanprover-community · Mar 24, 2023 · a569461 · a569461
1 parent 2077901
commit a569461
Show file tree

Hide file tree

Showing 4 changed files with 430 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -436,6 +436,7 @@ import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Linear.FunctorCategory
 import Mathlib.CategoryTheory.Linear.LinearFunctor
+import Mathlib.CategoryTheory.Localization.Construction
 import Mathlib.CategoryTheory.Monad.Basic
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.End