Theorem CategoryTheory.Grothendieck.functor_comp_forget

Modification history

2024-07-20 11:58
Mathlib/CategoryTheory/Grothendieck.lean
promoting the Grothendieck construction into a functor (#14387) …
Added CategoryTheory.Grothendieck.functor_comp_forgetView on Github →