Mathlib Changelog
v4
Changelog
About
Github
Theorem
CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app
Modification history
2024-07-08 20:11
Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
feat(CategoryTheory/Adjunction): left adjoint is faithful iff unit is mono, etc. (#14490) …
Added
CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app
View on Github →