Mathlib v3 is deprecated. Go to Mathlib v4

Def adj

Modification history

2021-07-09 15:19

src/algebra/category/Mon/adjunctions.lean

feat(algebra/category): provide right adjoint instances for forget (#8235) …

Added adj View on Github →