Mathlib Changelog
v4
Changelog
About
Github
Theorem
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app
Modification history
2024-04-26 15:11
Mathlib/CategoryTheory/Adjunction/Restrict.lean
chore(CategoryTheory/Adjunction): move `Adjunction.restrictFullyFaithful` to separate file (#12363) …
Added
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app
View on Github →