Commit 2024-04-27 23:30 0b522a14

View on Github →

fix(AlgebraicGeometry/GammaSpecAdjunction): speedup by adding universes (#12469) Add some explicit universe annotations because they cause a speedup (currently an unexplained phenomenon, unfortunately).

Estimated changes

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

modified theorem AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext

modified theorem AlgebraicGeometry.SpecΓIdentity_hom_app_presheaf_obj

modified theorem AlgebraicGeometry.SpecΓIdentity_naturality

modified theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app_app_top