Def CategoryTheory.equivEssImageOfReflective_counitIso_app

Modification history

2024-09-05 08:22

Mathlib/CategoryTheory/Adjunction/Reflective.lean

chore(CategoryTheory/Adjunction): address porting notes in `Reflective` file (#16089)

Deleted CategoryTheory.equivEssImageOfReflective_counitIso_app View on Github →

2023-02-24 18:15

Mathlib/CategoryTheory/Adjunction/Reflective.lean

feat: port CategoryTheory.Adjunction.Reflective (#2467)

Added CategoryTheory.equivEssImageOfReflective_counitIso_app View on Github →