Commit 2024-05-01 15:23 4fce67d3

View on Github →

perf(AG.RingHomProperties): less defeq abuse (#12563) We remove all uses (but one minor one) of erw in affineLocally_iff_affineOpens_le and add some explicit universe annotations. This speeds up the file by ~~50%~~ 40%.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

modified theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le

modified theorem RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion

modified theorem RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover

modified theorem RingHom.RespectsIso.basicOpen_iff

modified theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff