Commit 2024-09-05 08:22 7a1843ac

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

deleted def CategoryTheory.equivEssImageOfReflective_counitIso_app

deleted theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_hom

deleted theorem CategoryTheory.equivEssImageOfReflective_map_counitIso_app_inv

Modified Mathlib/CategoryTheory/EssentialImage.lean

added theorem CategoryTheory.Functor.essImage_ext