2025-10-25 11:48
Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
feat(CategoryTheory/Adjunction/PartialAdjunction): add symm naturality lemmas for HomEquiv and lift functor (#30143) …
Added CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm