Theorem CategoryTheory.Adjunction.isIso_unit_iff_isIso_counit

Modification history

2025-07-31 04:45
Mathlib/CategoryTheory/Adjunction/Triple.lean
feat(CategoryTheory/Adjunction): more results on adjoint triples. (#27650) …
Deleted CategoryTheory.Adjunction.isIso_unit_iff_isIso_counitView on Github →
2024-08-30 13:02
Mathlib/CategoryTheory/Adjunction/Triple.lean
feat(CategoryTheory/Adjunction): left adjoint in adjoint triple is fully faithful iff right adjoint is (#16167)
Added CategoryTheory.Adjunction.isIso_unit_iff_isIso_counitView on Github →