Theorem CategoryTheory.Grothendieck.comp_fiber'

Modification history

2024-10-26 14:30

Mathlib/CategoryTheory/Grothendieck.lean

feat(CategoryTheory/Grothendieck): `Grothendieck.pre` for Grothendieck construction base change (#18044) …

Deleted CategoryTheory.Grothendieck.comp_fiber'View on Github →

2024-07-20 11:58

Mathlib/CategoryTheory/Grothendieck.lean

promoting the Grothendieck construction into a functor (#14387) …

Added CategoryTheory.Grothendieck.comp_fiber'View on Github →