Def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso

Modification history

2024-04-27 09:23

Mathlib/CategoryTheory/Adjunction/Opposites.lean

chore(CategoryTheory): make `Functor.Full` a Prop (#12449) …

Modified CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso View on Github →

2023-03-28 22:14

Mathlib/CategoryTheory/Adjunction/Opposites.lean

feat: Port CategoryTheory.Adjunction.Opposites (#2424)

Added CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso View on Github →