Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-26 18:55 64aad5b8

View on Github →

feat(category_theory/adjunction): uniqueness of adjunctions (#3940) Co-authored by @thjread

Estimated changes

Modified src/category_theory/adjunction/basic.lean

Modified src/category_theory/adjunction/opposites.lean

added def adjunction.left_adjoint_uniq

added def adjunction.left_adjoints_coyoneda_equiv

added def adjunction.right_adjoint_uniq