feat: port CategoryTheory.Adjunction.Basic (#2198)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
leanprover-community · Feb 21, 2023 · 13138c8 · 13138c8
1 parent 3ce8f3f
commit 13138c8
Show file tree

Hide file tree

Showing 2 changed files with 678 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -221,6 +221,7 @@ import Mathlib.Algebra.Support
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Arrow
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Basic