Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.forget_adj_star

Modification history

2021-04-22 06:38

src/category_theory/adjunction/over.lean

feat(category_theory/adjunction): construct an adjunction on the over category (#7290) …

Added category_theory.forget_adj_star View on Github →