feat: port CategoryTheory.Enriched.Basic (#5154)

leanprover-community · Jun 17, 2023 · d063ef5 · d063ef5
1 parent 59f8374
commit d063ef5
Show file tree

Hide file tree

Showing 2 changed files with 476 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -822,6 +822,7 @@ import Mathlib.CategoryTheory.Elements
 import Mathlib.CategoryTheory.Elementwise
 import Mathlib.CategoryTheory.Endofunctor.Algebra
 import Mathlib.CategoryTheory.Endomorphism
+import Mathlib.CategoryTheory.Enriched.Basic
 import Mathlib.CategoryTheory.EpiMono
 import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Equivalence