Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 13:26 94d51b99

View on Github →

chore(algebraic_geometry/presheafed_space): Make has_colimits work faster (#10703)

Estimated changes

Modified src/algebraic_geometry/presheafed_space/has_colimits.lean

added theorem algebraic_geometry.PresheafedSpace.colimit_carrier

added def algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc

added theorem algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_fac

added theorem algebraic_geometry.PresheafedSpace.colimit_presheaf