Theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp_obj

Modification history

2025-06-16 08:15
Mathlib/CategoryTheory/FiberedCategory/Fiber.lean
feat(FiberedCategory/Grothendieck): the Grothendieck construction is fibered (#25645) …
Added CategoryTheory.Functor.Fiber.inducedFunctor_comp_objView on Github →