Theorem CategoryTheory.Grothendieck.map_obj

Modification history

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