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%.