Theorem CategoryTheory.Grothendieck.map_map

Modification history

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