Theorem CategoryTheory.Adjunction.faithful_R_of_epi_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.faithful_R_of_epi_counit_appView on Github →