Theorem CategoryTheory.Grothendieck.map_id_eq

Modification history

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