Def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse

Modification history

2024-11-30 19:56
Mathlib/CategoryTheory/Grothendieck.lean
feat(CategoryTheory): Relation between the Grothendieck construction and `AsSmall` (#19539)
Added CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverseView on Github →