Theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit

Modification history

2024-05-12 16:16

Mathlib/CategoryTheory/Adjunction/Opposites.lean

refactor(CategoryTheory/Adjunction): make uniqueness of adjoints independent of opposites (#12625)

Modified CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit View on Github →

2023-03-28 22:14

Mathlib/CategoryTheory/Adjunction/Opposites.lean

feat: Port CategoryTheory.Adjunction.Opposites (#2424)

Added CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit View on Github →