Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-26 16:48
5a2082d0
View on Github →
chore(category/grothendieck): split definition to avoid timeout (
#8871
) Helpful for
#8807
.
Estimated changes
Modified
src/category_theory/grothendieck.lean
added
def
category_theory.grothendieck.grothendieck_Type_to_Cat_functor
added
def
category_theory.grothendieck.grothendieck_Type_to_Cat_inverse