Commit 2026-07-02 16:39 53781e1d

View on Github →

chore(CategoryTheory/Adjunction/Basic): to_dual for Adjunction.comp (#41296) This PR tags Adjunction.comp with to_dual, which is now possible thanks to #40493.

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

modified theorem CategoryTheory.Adjunction.comp_counit_app

modified theorem CategoryTheory.Adjunction.comp_unit_app

Modified Mathlib/CategoryTheory/Adjunction/Mates.lean