Def CategoryTheory.Adjunction.restrictFullyFaithful

Modification history

2024-04-27 09:23
Mathlib/CategoryTheory/Adjunction/Restrict.lean
chore(CategoryTheory): make `Functor.Full` a Prop (#12449) …
Deleted CategoryTheory.Adjunction.restrictFullyFaithfulView on Github →
2024-04-26 15:11
Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
chore(CategoryTheory/Adjunction): move `Adjunction.restrictFullyFaithful` to separate file (#12363) …
Modified CategoryTheory.Adjunction.restrictFullyFaithfulView on Github →
2023-02-22 19:59
Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
feat: port CategoryTheory.Adjunction.FullyFaithful (#2418)
Added CategoryTheory.Adjunction.restrictFullyFaithfulView on Github →