Def CategoryTheory.Functor.LeftAdjointObjIsDefined

Modification history

2025-04-23 10:36

Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` (#22574) …

Deleted CategoryTheory.Functor.LeftAdjointObjIsDefined View on Github →

2024-10-23 02:43

Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

feat(CategoryTheory/Adjunction): the left partial adjoint (#17388) …

Added CategoryTheory.Functor.LeftAdjointObjIsDefined View on Github →